# [Why3-club] syntactic sugar

Alan Schmitt alan.schmitt at polytechnique.org
Mon Sep 24 11:57:33 CEST 2012

```Yannick Moy <moy at adacore.com> writes:

> On 09/24/2012 09:23 AM, Alan Schmitt wrote:
>
>> Using this, I get the error (on the "a[i][j]" syntax):
>>
>> Bad arity: symbol ([]) must be applied to 3 arguments, but is applied to
>> 2
>>
>> What am I doing wrong? And where can I find some documentation about
>> this syntactic sugar?
>
> I would expect something like a[i,j] instead of a[i][j], but the
> syntax of Why3 as documented in the manual only supports bracket
> notation with a single term inside the brackets. So it seems your use
> of brackets is not supported. (and the definition should be rejected
> in that case by Why3)

I finally decided to use pairs to define these matrices. For the record,
here is what I wrote.

** file pair.why

theory Pair

function fst (p : ('a, 'b)) : 'a =
match p with
| (a, b) -> a
end

function snd (p : ('a, 'b)) : 'b =
match p with
| (a, b) -> b
end

end

** file matrix.mlw

module Matrix

use import int.Int
use import pair.Pair as P
use import map.Map as M

type matrix 'a model {| xlength : int;
ylength : int;
mutable elts : map (int,int) 'a |}

function get (a: matrix 'a) (p: (int, int)) : 'a = M.get a.elts p

function set (a: matrix 'a) (p: (int, int)) (v: 'a) : matrix 'a =
{| a with elts = M.set a.elts p v |}

function ([]) (a: matrix 'a) (p: (int, int)) : 'a = get a p
function ([<-]) (a: matrix 'a) (p : (int, int)) (v: 'a) : matrix 'a = set a p v

val ([]) (a: matrix 'a) (p: (int,int)) :
{ 0 <= P.fst p < xlength a /\ 0 <= P.snd p < ylength a } 'a reads a { result = a[p] }

val ([]<-) (a: matrix 'a) (p: (int, int)) (v: 'a) :
{ 0 <= P.fst p < xlength a /\ 0 <= P.snd p < ylength a }
unit writes a
{ a.elts = M.set (old a.elts) p v }

val xlength (a: matrix 'a) : {} int { result = a.xlength }
val ylength (a: matrix 'a) : {} int { result = a.ylength }

val make (n: int) (m: int) (v: 'a) :
{ n >= 0 /\ m >= 0 }
matrix 'a
{ result = {| xlength = n; ylength = m; elts = M.const v |} }
end

I'm now using it for my maze, and I don't understand why I don't have to
prove some things. Here is the code where I use it:

module Maze

use import int.Int
use import module matrix.Matrix as M

predicate square_board (board : matrix int) =
board.xlength = board.ylength

let mk_board (n:int) =
{ n >= 0 }
M.make n n 0
{ forall i j : int. result[(i,j)] = 0 /\ square_board result}

end

When I generate the proof obligation, I only have to prove the
precondition of M.make (its first two arguments are greater than 0) and
the first postcondition of mk_board. For some reason, I don't have to
show that "square_board result" holds.

Am I using "predicate" in a wrong way?

Thanks,

Alan

```