[Why3-club] creating an array of arrays
alan.schmitt at polytechnique.org
Wed Sep 19 18:09:16 CEST 2012
I'm trying to write a small program that uses a board which I'm trying
to represent as an array of arrays. I'm able to specify that the board
is square, but I don't know how to create it. Here is what I tried:
use import int.Int
use import module array.Array
predicate square_board (board : array (array int)) =
forall i:int. 0 <= i < length board ->
length board[i] = length board
let mk_board (n:int) =
instead of "..." I tried "make n (make n 0)" and "make n (make 0 0)"
(with the latter hoping to replace the value of each slot with a freshly
allocated array), but I always get an error of the form "local reference
would escape its scope".
My question is twofold: is it possible to do this using arrays? If not,
what is the alternative? Creating a matrix module similar to the array
module? Or maybe directly use maps?
Thanks a lot,
More information about the Why3-club