Commit ddfa942e authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files

- Convert the syntax of prototype declarations and type expressions

  in the logic language into (more or less) higher-order style.
  For example,

    logic func (x : int, y : int, 'a list) : (int, 'a) map list

    logic pred (bool, int * real)

  is now written:
    
    logic func (x y : int) (list 'a) : list (map int 'a)

    logic pred bool (int, real)

  Note that types use prefix notation (as in Coq) and the types
  of tuples are now written as (type1, type2, ..., typeN).

- Use the same syntax of type expressions in the program language.

- Allow binders of the form (x y:int) in the program language.
  
parent 869cd9e9
......@@ -2,7 +2,7 @@
(* different relations *)
{
logic rel(int, int)
logic rel int int
}
let rec even (x:int) : int variant {x} for rel =
......
parameter incr : x:int ref -> { } unit writes x { !x = old !x + 1 }
parameter incr : x:ref int -> { } unit writes x { !x = old !x + 1 }
parameter x : int ref
parameter x : ref int
parameter id_not_0 : x:int -> { x <> 0 } int { result = x }
......@@ -48,8 +48,8 @@ let test_all_1 () =
logic d : int
}
parameter vx : int ref
parameter vy : int ref
parameter vx : ref int
parameter vy : ref int
parameter sq : x:int -> {} int { result = x*x }
......
exception Exception of int
parameter t : int ref
parameter t : ref int
parameter m : a:int -> b:int ->
{ }
......
......@@ -42,7 +42,7 @@ let p6 () =
(* composition of exceptions with side-effect on a reference *)
parameter x : int ref
parameter x : ref int
let p7 () =
{} begin x := 1; raise E; x := 2 end { false } | E -> { !x = 1 }
......
(** 1. A loop increasing [i] up to 10. *)
parameter i : int ref
parameter i : ref int
let loop1 (u:unit) =
{ !i <= 10 }
......@@ -14,7 +14,7 @@ let loop1 (u:unit) =
(** 2. The same loop, followed by a function call. *)
parameter x: int ref
parameter x: ref int
let negate (u:unit) = {} x := - !x { !x = -old(!x) }
......
{
logic q1(int, int, int)
logic q1 int int int
}
parameter r : int ref
parameter r : ref int
parameter f1 : y:int ->
{} unit writes r { q1 (!r) (old (!r)) y }
......@@ -11,14 +11,14 @@ parameter f1 : y:int ->
let g1 () = {} f1 !r { q1 (!r) (old (!r)) (old (!r)) }
{
logic foo(int) : int
logic q(int, int, int)
logic foo int : int
logic q int int int
}
parameter f : t:int ref -> x:int ->
parameter f : t:ref int -> x:int ->
{} unit reads t writes t { q (!t) (old (!t)) x }
let g (t:int ref) =
let g (t:ref int) =
{}
f t (foo !t)
{ q (!t) (old (!t)) (foo (old (!t))) }
......
(* Tests for proof obligations. *)
parameter x : int ref
parameter x : ref int
{
logic q(int)
......
......@@ -8,7 +8,7 @@ let rec f1 (x:int) : int variant { x } =
(** 2. With effects but no argument *)
parameter x : int ref
parameter x : ref int
let rec f2 (u:unit) : unit variant { !x } =
{ !x >= 0 } (if !x > 0 then begin x := !x - 1; f2 () end) { !x = 0 }
......@@ -22,7 +22,7 @@ let rec f3 (a:int) : unit variant { a } =
(** 4. With effects and a reference as argument *)
let rec f4 (a:int ref) : unit variant { !a } =
let rec f4 (a:ref int) : unit variant { !a } =
{ !a >= 0 }
if !a > 0 then begin x := !x + 1; a := !a - 1; f4 a end
{ !x = old !x + old !a }
......@@ -30,7 +30,7 @@ let rec f4 (a:int ref) : unit variant { !a } =
(** 5. The acid test:
partial application of a recursive function with effects *)
let rec f5 (a:int ref) (b:int ref) variant { !a } =
let rec f5 (a b:ref int) variant { !a } =
{ !a >= 0 }
if !a = 0 then !b else begin a := !a - 1; b := !b + 1; f5 a b end
{ result = old !a + old !b }
......
(* Side effect in expressions (Bart Jacobs' tricky example) *)
parameter b : int ref
parameter b1 : int ref
parameter b2 : int ref
parameter b : ref int
parameter b1 : ref int
parameter b2 : ref int
let f () =
{} b := 1 - !b; !b { result = !b and !b = 1 - old(!b) }
......
(* side effects in tests *)
parameter x : int ref
parameter x : ref int
parameter set_and_test_zero :
v:int ->
......@@ -13,7 +13,7 @@ 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:int ref) =
let p2 (y:ref int) =
{ !y >= 0 }
while set_and_test_nzero !y do
invariant { !y >= 0 } variant { !y }
......@@ -21,7 +21,7 @@ let p2 (y:int ref) =
done
{ !y = 0 }
let p3 (y:int ref) =
let p3 (y:ref int) =
{ !y >= 0 }
while let b = set_and_test_nzero !y in b do
invariant { !y >= 0 } variant { !y }
......@@ -29,7 +29,7 @@ let p3 (y:int ref) =
done
{ !y = 0 }
let p4 (y:int ref) =
let p4 (y:ref int) =
{ !y >= 1 }
while begin y := !y - 1; (set_and_test_nzero !y) end do
invariant { !y >= 1 } variant { !y }
......
parameter x : int ref
parameter x : ref int
parameter f : unit -> { } unit writes x { !x = 1 - old (!x) }
......
theory Test
type 'a t
type t 'a
type u = t
end
theory Test
type 'a t
type u = (int, int) t
type t 'a
type u = t int int
end
theory A
type 'a list = Nil | Cons('a, 'a list)
axiom A : forall l:int list. match l with Cons(x,x) -> true | Nil -> false end
type list 'a = Nil | Cons 'a (list 'a)
axiom A : forall l:int list. match l with Cons x x -> true | Nil -> false end
end
theory A
type 'a list = Nil | Cons('a, 'a list)
type list 'a = Nil | Cons 'a (list 'a)
axiom A : forall l:int list. (match l with Cons(x,x) -> 0 | Nil -> 1 end) = 2
axiom A : forall l:int list. (match l with Cons x x -> 0 | Nil -> 1 end) = 2
end
theory Test
type 'a t = 'b
type t 'a = 'b
end
theory Test
type 'a list = Nil
type list 'a = Nil
axiom Ax : Nil=Nil
end
theory Test
type 'a list = Nil | Cons('a, 'a list)
axiom Ax : Cons(Nil,Nil)=Nil
type list 'a = Nil | Cons 'a (list 'a)
axiom Ax : Cons Nil Nil = Nil
end
theory TreeForest
type 'a list = Nil | Cons('a, 'a list)
type 'a tree = Leaf('a) | Node('a forest)
type 'a forest = 'a tree list
type list 'a = Nil | Cons 'a (list 'a)
type tree 'a = Leaf 'a | Node (forest 'a)
type forest 'a = list (tree 'a)
end
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment