[Why3-club] request for comments

Andrei Paskevich andrei at tertium.org
Thu Sep 20 17:07:09 CEST 2012


Dear users,

We would like to make a change to the syntax of specifications in WhyML.
Before doing so, we would appreciate comments from our users,
especially those who produce Why3 syntax automatically (e.g. Adacore)
as well as those who already have a corpus of WhyML programs.

Our motivation is:
- to give the possibility to gather all specification clauses for a
   given function at the same place (to day, the postcondition must be
   placed after the function body), so that it is easier to
   add/remove/comment out a function specification;

- to make a clearer distinction with record syntax
   (we have to admit that f x = {a=b}{|c=d|}{e=f} is hardly readable);

- to be able to use standard curly braces for records.

The changes of syntax would be as follows:

spec   ::= clause*

clause ::= "requires" "{" fmla "}"
          | "ensures"  "{" fmla "}"
          | "returns"  "{" pat "->" fmla "|" ... "|" pat "->" fmla "}"
          | ["ghost"] "raises"
              "{" X pat "->" fmla "|" ... "|" X pat "->" fmla "}"
          | ["ghost"] "reads"    p "," ... "," p
          | ["ghost"] "writes"   p "," ... "," p
          | variant

variant ::= "variant" "{" t ["with" rel] "," ... "," t ["with" rel] "}"

p ::= x | p "." x

expr ::= "any" type spec
        | "abstract" expr spec
        | "while" expr "do"
            ("invariant" "{" fmla "}" | variant)* expr "done"
        | "let" ["rec"] ident signature "="  body "in" expr
        | "fun"               signature "->" body
        | ...

body ::= spec expr spec

signature ::= (arg spec)* arg [":" type] spec

decl ::= "val" ["rec"] ident signature ["=" body]
        | "val" ident ":" type

Comments:
- higher-order types are no more written using arrows.
- construct "any" cannot introduce a function anymore.
- "val" replaces "let" for toplevel definitions
- in a function definition, specification clauses can be placed before
   "=", between "=" and function body, and after function body
- specification clauses are now cumulative i.e. multiple "requires",
   "ensures", etc. are allowed (and are interpreted as conjunctions),
   with the only exception of variants

To turn current WhyML code into this new syntax will require the
following (mostly local) operations:
- insert "requires" and "ensures" keywords in front of pre- and
postconditions (it is not required to move postconditions to the
beginning of function definitions)
- in function definitions, insert "raises" in front of exceptional
postconditions
- in function declarations, merge "raises" and exceptional postconditions
- in function declarations, return type must be moved before the
precondition

Best regards,
--
Andrei and Jean-Christophe
-------------- next part --------------
(** {1 Arrays} *)

(** {2 Generic Arrays}

The length is a non-mutable field, so that we get for free that
modification of an array does not modify its length.

*)

module Array

  use import int.Int
  use import map.Map as M

  type array 'a model { length : int; mutable elts : map int 'a }

  function get (a: array 'a) (i: int) : 'a = M.get a.elts i

  function set (a: array 'a) (i: int) (v: 'a) : array 'a =
    { a with elts = M.set a.elts i v }

  (** syntactic sugar *)
  function ([]) (a: array 'a) (i: int) : 'a = get a i
  function ([<-]) (a: array 'a) (i: int) (v: 'a) : array 'a = set a i v

  val ([]) (a: array 'a) (i: int) : 'a
    requires { 0 <= i < length a } reads a ensures { result = a[i] }

  val ([]<-) (a: array 'a) (i: int) (v: 'a) : unit
    requires { 0 <= i < length a }
    writes   a
    ensures  { a.elts = M.set (old a.elts) i v }

  val length (a: array 'a) : int
    ensures { result = a.length }

  (** unsafe get/set operations with no precondition *)
  exception OutOfBounds

  val defensive_get (a: array 'a) (i: int) =
    if i < 0 || i >= length a then raise OutOfBounds;
    a[i]
    ensures { 0 <= i < length a /\ result = a[i] }
    raises  { OutOfBounds -> i < 0 \/ i >= length a }

  val defensive_set (a: array 'a) (i: int) (v: 'a) =
    if i < 0 || i >= length a then raise OutOfBounds;
    a[i] <- v
    ensures { 0 <= i < length a /\ a = (old a)[i <- v] }
    raises  { OutOfBounds -> i < 0 \/ i >= length a }

  val make (n: int) (v: 'a) : array 'a
    requires { n >= 0 }
    ensures  { result = { length = n; elts = M.const v } }

  val append (a1: array 'a) (a2: array 'a) : array 'a
    ensures { length result = length a1 + length a2 }
    ensures { forall i:int. 0 <= i < length a1 -> result[i] = a1[i] }
    ensures { forall i:int. 0 <= i < length a2 -> result[length a1 + i] = a2[i]}

  val sub (a: array 'a) (ofs: int) (len: int) : array 'a
    requires { 0 <= ofs /\ ofs + len <= length a }
    ensures  { length result = len }
    ensures  { forall i:int. 0 <= i < len -> result[i] = a[ofs + i] }

  val copy (a: array 'a) : array 'a
    ensures { length result = length a /\
      forall i:int. 0 <= i < length result -> result[i] = a[i] }

  let fill (a: array 'a) (ofs: int) (len: int) (v: 'a) =
    requires { 0 <= ofs /\ ofs + len <= length a }
    ensures  { forall i:int. (0 <= i < ofs \/ ofs + len <= i < length a) ->
               a[i] = (old a)[i] }
    ensures  { forall i:int. ofs <= i < ofs + len -> a[i] = v }
'Init:
    for k = 0 to len - 1 do
      invariant { forall i:int. (0 <= i < ofs \/ ofs + len <= i < length a) ->
                  a[i] = (at a 'Init)[i] }
      invariant { forall i:int. ofs <= i < ofs + k -> a[i] = v }
      a[ofs + k] <- v
    done

  val blit (a1: array 'a) (ofs1: int)
                 (a2: array 'a) (ofs2: int) (len: int) : unit
    requires { 0 <= ofs1 /\ ofs1 + len <= length a1 /\
      0 <= ofs2 /\ ofs2 + len <= length a2 }
    writes a2
    ensures { (forall i:int.
        (0 <= i < ofs2 \/ ofs2 + len <= i < length a2) -> a2[i] = (old a2)[i])
      /\
      (forall i:int.
        ofs2 <= i < ofs2 + len -> a2[i] = a1[ofs1 + i - ofs2]) }

end


(***
Local Variables:
compile-command: "unset LANG; make -C .. modules/array"
End:
*)



More information about the Why3-club mailing list