programs: regions in progress

parent 65a92cec
......@@ -55,6 +55,9 @@ why.conf
/bin/why3doc.byte
/bin/why3doc.opt
/bin/why3doc
/bin/why3replayer.byte
/bin/why3replayer.opt
/bin/why3replayer
# /doc/
/doc/version.tex
......
......@@ -855,8 +855,8 @@ testl: bin/why3ml.byte
ocamlrun -bt bin/why3ml.byte tests/test-pgm-jcf.mlw
ocamlrun -bt bin/why3ml.byte -P alt-ergo tests/test-pgm-jcf.mlw
testl-debug: bin/why3ml.byte
ocamlrun -bt bin/why3ml.byte --debug-all --debug program_typing tests/test-pgm-jcf.mlw
testl-debug: bin/why3ml.opt
bin/why3ml.opt --debug program_typing tests/test-pgm-jcf.mlw
testl-ide: bin/why3ide.opt
bin/why3ide.opt tests/test-pgm-jcf.mlw
......
......@@ -3,6 +3,6 @@ module M
use import module stdlib.Ref
parameter f : x:int -> {} unit writes a {}
parameter f : x:int -> {} unit writes a.contents {}
end
......@@ -3,6 +3,6 @@ module M
use import module stdlib.Ref
parameter f : x:int -> {} unit writes x {}
parameter f : x:int -> {} unit writes x.contents {}
end
......@@ -5,6 +5,6 @@ module M
parameter a : int
parameter f : x:int -> {} unit writes a {}
parameter f : x:int -> {} unit writes a.contents {}
end
......@@ -5,6 +5,6 @@ module M
parameter foo : int -> int
parameter f : x:int -> {} unit writes foo {}
parameter f : x:int -> {} unit writes foo.contents {}
end
......@@ -3,7 +3,7 @@ module M
use import int.Int
use import module stdlib.Ref
parameter incr : x:ref int -> { } unit writes x { x = old x + 1 }
parameter incr : x:ref int -> { } unit writes x.contents { x = old x + 1 }
parameter x : ref int
......
......@@ -8,7 +8,7 @@ parameter t : ref int
parameter m : a:int -> b:int ->
{ }
unit reads t raises Exception
unit reads t.contents raises Exception
{ true } | Exception -> { true }
let test () =
......
......@@ -4,23 +4,23 @@ module M
logic q1 int int int
parameter r : ref int
parameter r : ref int
parameter f1 : y:int ->
{} unit writes r { q1 r (old r) y }
parameter f1 : y:int ->
{} unit writes r.contents { q1 r (old r) y }
let g1 () = {} f1 !r { q1 r (old r) (old r) }
let g1 () = {} f1 !r { q1 r (old r) (old r) }
logic foo int : int
logic q int int int
parameter f : t:ref int -> x:int ->
{} unit reads t writes t { q t (old t) x }
parameter f : t:ref int -> x:int ->
{} unit writes t.contents { q t (old t) x }
let g (t:ref int) =
{}
f t (foo !t)
{ q t (old t) (foo (old t)) }
let g (t:ref int) =
{}
f t (foo !t)
{ q t (old t) (foo (old t)) }
end
......
......@@ -49,7 +49,7 @@ let p11a () = {} let a = (fsucc 1) in a + a { result = 4 }
(* function with a post-condition and side-effects *)
parameter incrx : unit -> { } unit writes x { x = (old x) + 1 }
parameter incrx : unit -> { } unit writes x.contents { x = (old x) + 1 }
let p12 () = { x = 0 } incrx () { x = 1 }
......@@ -59,7 +59,7 @@ let p13a () = {} incrx (incrx ()) { x = (old x) + 2 }
(* function with side-effects, result and post-condition *)
parameter incrx2 : unit -> { } int writes x { x = old x + 1 and result = x }
parameter incrx2 : unit -> { } int writes x.contents { x = old x + 1 and result = x }
let p14 () = { x = 0 } incrx2 () { result = 1 }
......
module M
use import int.Int
use import module stdlib.Ref
(* side effects in tests *)
parameter x : ref int
parameter set_and_test_zero :
v:int ->
{} bool writes x { x = v and if result=True then x = 0 else x <> 0 }
let p () = {} if set_and_test_zero 0 then 1 else 2 { result = 1 }
parameter set_and_test_nzero :
v:int ->
{} bool writes x { x = v and if result=True then x <> 0 else x = 0 }
let p2 (y:ref int) =
{ y >= 0 }
while set_and_test_nzero !y do
invariant { y >= 0 } variant { y }
y := !y - 1
done
{ y = 0 }
let p3 (y:ref int) =
{ y >= 0 }
while let b = set_and_test_nzero !y in b do
invariant { y >= 0 } variant { y }
y := !y - 1
done
{ y = 0 }
let p4 (y:ref int) =
{ y >= 1 }
while begin y := !y - 1; (set_and_test_nzero !y) end do
invariant { y >= 1 } variant { y }
()
done
{ y = 0 }
use import int.Int
use import module stdlib.Ref
(* side effects in tests *)
parameter x : ref int
parameter set_and_test_zero :
v:int ->
{}
bool writes x.contents
{ x = v and if result=True then x = 0 else x <> 0 }
let p () = {} if set_and_test_zero 0 then 1 else 2 { result = 1 }
parameter set_and_test_nzero :
v:int ->
{}
bool writes x.contents
{ x = v and if result=True then x <> 0 else x = 0 }
let p2 (y:ref int) =
{ y >= 0 }
while set_and_test_nzero !y do
invariant { y >= 0 } variant { y }
y := !y - 1
done
{ y = 0 }
let p3 (y:ref int) =
{ y >= 0 }
while let b = set_and_test_nzero !y in b do
invariant { y >= 0 } variant { y }
y := !y - 1
done
{ y = 0 }
let p4 (y:ref int) =
{ y >= 1 }
while begin y := !y - 1; (set_and_test_nzero !y) end do
invariant { y >= 1 } variant { y }
()
done
{ y = 0 }
end
......
......@@ -5,7 +5,7 @@ use import module stdlib.Ref
parameter x : ref int
parameter f : unit -> { } unit writes x { x = 1 - old x }
parameter f : unit -> { } unit writes x.contents { x = 1 - old x }
let p () =
begin
......
theory Misfix
type t
logic ([]) (a: t) (i: int) : int
logic ([<-]) (a: t) (i: int) (v: int) : t
axiom a1 : forall a: t, i v: int. a[i <- v][i] = v
axiom a2 : forall a: t, i j v: int. i<>j -> a[i <- v][j] = a[j]
goal g1 : forall a: t, i j v: int. a[a[i] <- i][a[i]] = i
end
......@@ -22,7 +22,7 @@ module Algo63
parameter partition :
a : array int -> m:int -> n:int -> i:ref int -> j:ref int ->
{ m < n }
unit writes a i j
unit writes a.contents i.contents j.contents
{ m <= j and j < i and i <= n and permut (old a) a m n and
exists x:int.
(forall r:int. m <= r <= j -> a[r] <= x) and
......
......@@ -25,7 +25,7 @@ module Algo64
parameter partition :
a : array int -> m:int -> n:int -> i:ref int -> j:ref int ->
{ 0 <= m < n < length a }
unit writes a i j
unit writes a.contents i.contents j.contents
{ m <= j < i <= n and permut (old a) a m n and
exists x:int.
(forall r:int. m <= r <= j -> a[r] <= x) and
......
......@@ -24,7 +24,7 @@ module Algo65
parameter partition :
a : array int -> m:int -> n:int -> i:ref int -> j:ref int ->
{ 0 <= m < n < length a }
unit writes a i j
unit writes a.contents i.contents j.contents
{ m <= j < i <= n and permut (old a) a m n and
exists x:int.
(forall r:int. m <= r <= j -> a[r] <= x) and
......
......@@ -4,11 +4,12 @@
module M
use import module stdlib.Refint
use import array.ArrayLength
use import module stdlib.Array
parameter a : array int
logic inv (a : t int int) =
logic inv (a : map int) =
a[0] = 0 and length a = 11 and forall k:int. 1 <= k <= 10 -> 0 < a[k]
parameter loop1 : ref int
......@@ -30,8 +31,8 @@ module M
variant { j }
(* ghost *) incr loop2;
let temp = a[!j] in
a[!j <- a[!j - 1]];
a[!j - 1 <- temp];
set a !j a[!j - 1];
set a (!j - 1) temp;
decr j
done;
incr i
......@@ -48,9 +49,9 @@ module ARM
(* memory *)
parameter mem : ref (t int int)
parameter mem_ldr : a:int -> {} int reads mem { result = mem[a] }
parameter mem_ldr : a:int -> {} int reads mem.contents { result = mem[a] }
parameter mem_str : a:int -> v:int ->
{} int writes mem { mem = (old mem)[a <- v] }
{} int writes mem.contents { mem = (old mem)[a <- v] }
(* data segment *)
(*
......@@ -70,16 +71,16 @@ module ARM
parameter pc : ref int (* pc *)
parameter ldr :
r:ref int -> a:int -> {} unit reads mem writes r { r = mem[a] }
r:ref int -> a:int -> {} unit reads mem.contents writes r.contents { r = mem[a] }
parameter str :
r:ref int -> a:int -> {} unit reads r writes mem { mem = (old mem)[a <- r] }
r:ref int -> a:int -> {} unit reads r.contents writes mem.contents { mem = (old mem)[a <- r] }
(* condition flags *)
parameter le : ref bool
parameter cmp : r:ref int -> v:int ->
{}
unit reads r writes le
unit reads r.contents writes le.contents
{ le=True <-> r <= v }
end
......
theory Order
type t
logic (<=) t t
axiom le_refl : forall x : t. x <= x
axiom le_asym : forall x y : t. x <= y -> y <= x -> x = y
axiom le_trans: forall x y z : t. x <= y -> y <= z -> x <= z
end
theory List
type list 'a = Nil | Cons 'a (list 'a)
logic mem (x: 'a) (l: list 'a) = match l with
| Nil -> false
| Cons y r -> x = y \/ mem x r
end
end
theory SortedList
use import List
clone import Order as O
inductive sorted (l : list t) =
| sorted_nil :
sorted Nil
| sorted_one :
forall x:t. sorted (Cons x Nil)
| sorted_two :
forall x y : t, l : list t.
x <= y -> sorted (Cons y l) -> sorted (Cons x (Cons y l))
lemma sorted_mem:
forall x: t, l: list t. sorted (Cons x l) ->
forall y: t. mem y l -> x <= y
end
theory SortedIntList
use import int.Int
use import List
clone import SortedList with type O.t = int, logic O.(<=) = (<=)
goal sorted123: sorted (Cons 1 (Cons 2 (Cons 3 Nil)))
end
......@@ -7,7 +7,7 @@ module Queue
use import list.Append
use import list.Length
mutable type t 'a model list 'a
type t 'a model {| mutable contents : list 'a |}
parameter create : unit -> {} t 'a { result = Nil }
......
......@@ -6,7 +6,7 @@ module Stack
use import list.List
use import list.Length
mutable type t 'a model list 'a
type t 'a model {| mutable contents : list 'a |}
parameter create : unit -> {} t 'a { result = Nil }
......
......@@ -3,13 +3,13 @@
module Ref
mutable type ref 'a model 'a
type ref 'a = {| mutable contents : 'a |}
parameter ref : v:'a -> {} ref 'a { result=v }
parameter (!) : r:ref 'a -> {} 'a reads r { result=r }
parameter (!) : r:ref 'a -> {} 'a reads r.contents { result=r }
parameter (:=) : r:ref 'a -> v:'a -> {} unit writes r { r=v }
parameter (:=) : r:ref 'a -> v:'a -> {} unit writes r.contents { r=v }
end
......@@ -18,33 +18,62 @@ module Refint
use export int.Int
use export module Ref
parameter incr : r:ref int -> {} unit writes r { r = old r + 1 }
parameter incr : r:ref int -> {} unit writes r.contents { r = old r + 1 }
parameter decr : r:ref int -> {} unit writes r { r = old r - 1 }
parameter decr : r:ref int -> {} unit writes r.contents { r = old r - 1 }
end
(* Arrays *)
module Array
use import int.Int
use export array.ArrayLength
use import array.ArrayLength as A
use import module Ref
type map 'a = t int 'a
type array 'a model ref (map 'a)
mutable type array 'a model t int 'a
logic length (a : array 'a) : int = A.length a
logic ([]) (a : array 'a) (i : int) : 'a = get a i
parameter ([]) : a:array 'a -> i:int ->
{ 0 <= i < length a } 'a reads a { result = a[i] }
{ 0 <= i < length a } 'a reads a.contents { result = a[i] }
parameter ([<-]) : a:array 'a -> i:int -> v:'a ->
{ 0 <= i < length a } unit writes a { a = (old a)[i <- v] }
parameter set : a:array 'a -> i:int -> v:'a ->
{ 0 <= i < length a } unit writes a.contents { a = (old a)[i <- v] }
parameter length : a:array 'a -> {} int reads a { result = length a }
parameter length : a:array 'a -> {} int { result = length a }
parameter make : n:int -> v:'a ->
{}
array 'a
parameter make : n:int -> v:'a ->
{}
array 'a
{ length result = n and forall i:int. 0 <= i < n -> result[i] = v}
end
(***
module Array
use import int.Int
use import array.Array
type map 'a = t int 'a
type array 'a model {| length : int; mutable elts : map 'a |}
logic ([]) (a : array 'a) (i : int) : 'a = get a.elts i
parameter ([]) : a:array 'a -> i:int ->
{ 0 <= i < a.length } 'a reads a.elts { result = a[i] }
parameter set : a:array 'a -> i:int -> v:'a ->
{ 0 <= i < a.length } unit writes a.elts { a.elts = (old a.elts)[i <- v] }
parameter length : a:array 'a -> {} int { result = a.length }
parameter make : n:int -> v:'a ->
{}
array 'a
{ result.length = n and forall i:int. 0 <= i < n -> result[i] = v}
parameter append : a1:array 'a -> a2:array 'a ->
{}
......@@ -68,10 +97,10 @@ module Array
parameter fill : a:array 'a -> ofs:int -> len:int -> v:'a ->
{ 0 <= ofs and ofs + len <= length a }
unit
writes a
{ (forall i:int.
(0 <= i < ofs or ofs + len <= i < length a) -> a[i] = (old a)[i])
and
writes a.elts
{ (forall i:int.
(0 <= i < ofs or ofs + len <= i < length a) -> a[i] = (old a)[i])
and
(forall i:int.
ofs <= i < ofs + len -> a[i] = v) }
......@@ -80,10 +109,10 @@ module Array
{ 0 <= ofs1 and ofs1 + len <= length a1 and
0 <= ofs2 and ofs2 + len <= length a2 }
unit
writes a2
{ (forall i:int.
(0 <= i < ofs2 or ofs2 + len <= i < length a2) -> a2[i] = (old a2)[i])
and
writes a2.elts
{ (forall i:int.
(0 <= i < ofs2 or ofs2 + len <= i < length a2) -> a2[i] = (old a2)[i])
and
(forall i:int.
ofs2 <= i < ofs2 + len -> a2[i] = a1[ofs1 + i - ofs2]) }
......@@ -103,7 +132,7 @@ module TestArray
let test_append () =
let a1 = make 17 2 in
assert { a1[3] = 2 };
a1[3 <- 4];
set a1 3 4;
assert { a1[3] = 4 };
let a2 = make 25 3 in
assert { a2[0] = 3 }; (* needed to prove a[17]=3 below *)
......@@ -129,6 +158,7 @@ module TestArray
assert { a2[24] = False }
end
***)
(*
Local Variables:
......
......@@ -3,7 +3,7 @@ module Char
use import int.Int
abstract type char model int
type char model int
parameter chr : x:int -> { 0 <= x <= 255 } char { result = x }
......@@ -35,9 +35,9 @@ module String
use import int.Int
use import module Char
use array.ArrayRich as S
use array.Array as S
mutable type string model S.t int char
type string model {| length : int; mutable chars : S.t int char |}
parameter create : len:int -> { len >= 0 } string { S.length result = len }
......@@ -94,9 +94,9 @@ module Buffer
use import module Char
use import module String
mutable type t model S.t int char
type t model {| length : int; mutable contents : S.t int char |}
parameter create : size:int -> { size >= 0 } t { S.length result = 0 }
parameter create : size:int -> { size >= 0 } t { result.length = 0 }
(** [size] is only given as a hint for the initial size *)
parameter contents : b:t -> { } string { result = b }
......
......@@ -572,7 +572,7 @@ let w = GWindow.window
~allow_grow:true ~allow_shrink:true
~width:gconfig.window_width
~height:gconfig.window_height
~title:"why GUI with database" ()
~title:"Why3" ()
let (_ : GtkSignal.id) = w#connect#destroy ~callback:exit_function
......
......@@ -26,6 +26,7 @@ open Theory
type type_var
val find_type_var : loc:Ptree.loc -> type_var Htv.t -> tvsymbol -> type_var
val create_ty_decl_var : ?loc:Ptree.loc -> user:bool -> tvsymbol -> type_var
type dty
......
......@@ -231,6 +231,8 @@ rule token = parse
{ SEMICOLON }
| "->"
{ ARROW }
| "<-"
{ LARROW }
| "<->"
{ LRARROW }
| "&&"
......
......@@ -177,7 +177,7 @@
%token COLON COMMA
%token DOT EQUAL FUNC LAMBDA LTGT
%token LEFTPAR LEFTPAR_STAR_RIGHTPAR LEFTREC LEFTSQ
%token LRARROW
%token LARROW LRARROW
%token PRED QUOTE
%token RIGHTPAR RIGHTREC RIGHTSQ
%token TILDE UNDERSCORE
......@@ -207,13 +207,14 @@
%right ARROW IMPLIES LRARROW IFF
%right OR BARBAR
%right AND AMPAMP
%nonassoc NOT
%nonassoc NOT TILDE
%left EQUAL LTGT OP1
%nonassoc RIGHTSQ /* stronger than OP1 for e1[e2 op1 e3] */
%nonassoc LARROW
%nonassoc RIGHTSQ /* stronger than <- for e1[e2 <- e3] */
%left OP2
%left OP3
%left OP4
%nonassoc prefix_op
%nonassoc prec_prefix_op
%left prec_app
%nonassoc LEFTSQ
%nonassoc OPPREF
......@@ -379,8 +380,9 @@ list1_type_decl:
type_decl:
| lident labels type_args typedefn
{ { td_loc = floc (); td_ident = add_lab $1 $2;
td_params = $3; td_def = $4 } }
{ let model, def = $4 in
{ td_loc = floc (); td_ident = add_lab $1 $2;
td_params = $3; td_model = model; td_def = def } }
;
type_args:
......@@ -389,11 +391,16 @@ type_args:
;
typedefn:
| /* epsilon */ { TDabstract }
| EQUAL primitive_type { TDalias $2 }
| EQUAL typecases { TDalgebraic $2 }
| EQUAL BAR typecases { TDalgebraic $3 }
| EQUAL record_type { TDrecord $2 }
| /* epsilon */ { false, TDabstract }
| equal_model primitive_type { $1, TDalias $2 }
| equal_model typecases { $1, TDalgebraic $2 }
| equal_model BAR typecases { $1, TDalgebraic $3 }
| equal_model record_type { $1, TDrecord $2 }
;
equal_model:
| EQUAL { false }
| MODEL { true }
;
record_type:
......@@ -548,7 +555,7 @@ lexpr:
{ mk_pp (PPinfix ($1, mk_id (infix $2) (floc_i 2), $3)) }
| lexpr OP4 lexpr
{ mk_pp (PPinfix ($1, mk_id (infix $2) (floc_i 2), $3)) }
| any_op lexpr %prec prefix_op
| prefix_op lexpr %prec prec_prefix_op
{ mk_pp (PPapp (Qident (mk_id (prefix $1) (floc_i 2)), [$2])) }
| qualid list1_lexpr_arg
{ mk_pp (PPapp ($1, $2)) }
......@@ -611,7 +618,7 @@ lexpr_arg:
;
lexpr_dot:
| lqualid_rich
| lqualid_poor
{ mk_pp (PPvar $1) }
| OPPREF lexpr_dot
{ mk_pp (PPapp (Qident (mk_id (prefix $1) (floc_i 2)), [$2])) }
......@@ -620,7 +627,7 @@ lexpr_dot:
;
lexpr_sub:
| lexpr_dot DOT lqualid
| lexpr_dot DOT lqualid_rich
{ mk_pp (PPapp ($3, [$1])) }
| LEFTPAR lexpr RIGHTPAR
{ $2 }
......@@ -634,9 +641,8 @@ lexpr_sub:
{ mk_pp (PPupdate ($2, List.rev $4)) }
| lexpr_arg LEFTSQ lexpr RIGHTSQ
{ mk_pp (PPapp (Qident (mk_id (misfix "[]") (floc ())), [$1; $3])) }
| lexpr_arg LEFTSQ lexpr OP1 lexpr RIGHTSQ
{ let op = "[" ^ $4 ^ "]" in
mk_pp (PPapp (Qident (mk_id (misfix op) (floc ())), [$1; $3; $5])) }
| lexpr_arg LEFTSQ lexpr LARROW lexpr RIGHTSQ
{ mk_pp (PPapp (Qident (mk_id (misfix "[<-]") (floc ())), [$1; $3; $5])) }
;
quant:
......@@ -806,14 +812,14 @@ lident_rich:
{ mk_id (infix $2) (floc ()) }
| LEFTPAR_STAR_RIGHTPAR
{ mk_id (infix "*") (floc ()) }
| LEFTPAR lident_op UNDERSCORE RIGHTPAR
| LEFTPAR prefix_op UNDERSCORE RIGHTPAR
{ mk_id (prefix $2) (floc ()) }
| LEFTPAR OPPREF RIGHTPAR
{ mk_id (prefix $2) (floc ()) }
| LEFTPAR LEFTSQ RIGHTSQ RIGHTPAR
{ mk_id (misfix "[]") (floc ()) }
| LEFTPAR LEFTSQ OP1 RIGHTSQ RIGHTPAR
{ mk_id (misfix ("[" ^ $3 ^ "]")) (floc ()) }
| LEFTPAR LEFTSQ LARROW RIGHTSQ RIGHTPAR
{ mk_id (misfix "[<-]") (floc ()) }
;
lident:
......@@ -822,14 +828,14 @@ lident:
;
lident_op:
| OP1 { $1 }
| OP2 { $1 }
| OP3 { $1 }
| OP4 { $1 }
| EQUAL { "=" }
| OP1 { $1 }
| OP2 { $1 }
| OP3 { $1 }
| OP4 { $1 }
| EQUAL { "=" }
;
any_op:
prefix_op:
| OP1 { $1 }
| OP2 { $1 }
| OP3 { $1 }
......@@ -873,6 +879,11 @@ lqualid_rich:
| uqualid DOT lident_rich { Qdot ($1, $3) }
;
lqualid_poor:
| lident { Qident $1 }
| uqualid DOT lident { Qdot ($1, $3) }
;
qualid:
| ident_rich { Qident $1 }
| uqualid DOT ident_rich { Qdot ($1, $3) }
......@@ -968,7 +979,7 @@ program_decl:
{ Dlet (add_lab $2 $3, mk_expr_i 8 (Efun ($6, $8))) }
| LET REC list1_recfun_sep_and
{ Dletrec $3 }
| PARAMETER lident_rich labels COLON type_v
| PARAMETER lident_rich_pgm labels COLON type_v
{ Dparam (add_lab $2 $3, $5) }
| EXCEPTION uident labels
{ Dexn (add_lab $2 $3, None) }
......@@ -978,22 +989,13 @@ program_decl:
{ $2 }
| NAMESPACE namespace_import namespace_name list0_program_decl END
{ Dnamespace (floc_i 3, $3, $2, $4) }
| ABSTRACT TYPE lident type_args model
{ Dmodel_type (false, $3, $4, $5) }
| MUTABLE TYPE lident type_args model
{ Dmodel_type (true, $3, $4, $5) }
| TYPE lident labels type_args EQUAL
LEFTBRC list1_field_decl opt_semicolon RIGHTBRC
{ Drecord_type (add_lab $2 $3, $4, $7) }