[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
More information about the Why3-club
mailing list