[Why3-club] creating an array of arrays

Alan Schmitt alan.schmitt at polytechnique.org
Wed Sep 19 18:09:16 CEST 2012

Hi again,

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:

module Maze
  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[0]

  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 mailing list