[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