un premier programme dans examples

parent acc655bd
......@@ -162,6 +162,9 @@ bin/why.static: $(CMX) src/why.cmx
bin/top: $(CMO)
ocamlmktop $(BFLAGS) -o $@ nums.cma $^
# test targets
##############
test: bin/why.byte $(TOOLS)
mkdir -p output_why3
ocamlrun -bt bin/why.byte -I theories/ --driver drivers/why3.drv \
......@@ -181,6 +184,9 @@ test: bin/why.byte $(TOOLS)
testl: bin/whyl.byte
ocamlrun -bt bin/whyl.byte -I theories/ src/programs/test.mlw
examples/programs/%: bin/whyl.byte
bin/whyl.byte -I theories examples/programs/$*.mlw
# programs
##########
......
(* Parameters.
Without loss of generality, we can take [x1=0] and [y1=0].
Thus the line to draw joins [(0,0)] to [(x2,y2)]
and we have [deltax = x2] and [deltay = y2].
Moreover we assume being in the first octant, i.e.
[0 <= y2 <= x2] (see the Coq file). The seven other cases can be easily
deduced by symmetry. *)
{
logic x2 : int
logic y2 : int
axiom First_octant : 0 <= y2 and y2 <= x2
}
(* Global variables of the program. *)
(* The code.
[(best x y)] expresses that the point [(x,y)] is the best
possible point i.e. the closest to the real line (see the Coq file).
The invariant relates [x], [y] and [e] and
gives lower and upper bound for [e] (see the Coq file). *)
{
use import int.Abs
logic best(x:int, y:int) =
forall y':int. abs (x2 * y - x * y2) <= abs (x2 * y' - x * y2)
logic invariant(x:int, y:int, e:int) =
e = 2 * (x + 1) * y2 - (2 * y + 1) * x2 and
2 * (y2 - x2) <= e and e <= 2 * y2
lemma Invariant_is_ok : forall x,y,e:int. invariant(x,y,e) -> best(x,y)
}
let bresenham =
let x = ref 0 in
let y = ref 0 in
let e = ref (2 * y2 - x2) in
while !x <= x2 do
invariant {0 <= !x and !x <= x2 + 1 and invariant(!x, !y, !e) }
variant { x2 + 1 - !x }
(* here we would do (plot x y) *)
assert { best(!x, !y) };
if !e < 0 then
e := !e + 2 * y2
else begin
y := !y + 1;
e := !e + 2 * (y2 - x2)
end;
x := !x + 1
done
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. testl"
End:
*)
......@@ -787,15 +787,20 @@ let add_logics dl th =
let dl = List.map type_decl dl in
List.fold_left add_decl th (create_logic_decls dl)
let env_of_denv denv =
Mstr.mapi
(fun x dty -> create_vsymbol (id_fresh x) (ty_of_dty dty))
denv.dvars
let type_term denv t =
let t = dterm denv t in
term Mstr.empty t
term (env_of_denv denv) t
let term uc = type_term (create_denv uc)
let type_fmla denv f =
let f = dfmla denv f in
fmla Mstr.empty f
fmla (env_of_denv denv) f
let fmla uc = type_fmla (create_denv uc)
......
......@@ -156,8 +156,16 @@ rule token = parse
{ ARROW }
| "="
{ EQUAL }
| "<>" | "<" | "<=" | ">" | ">=" as s
{ OP0 s }
| "<>"
{ OP0 "ne" }
| "<"
{ OP0 "lt" }
| "<="
{ OP0 "le" }
| ">"
{ OP0 "gt" }
| ">="
{ OP0 "ge" }
| "+" | "-" as c
{ OP2 (String.make 1 c) }
| "*" | "/" | "%" as c
......
......@@ -57,6 +57,10 @@
let id = { id = infix op; id_loc = loc_i 2 } in
mk_expr (mk_apply_id id [e1; e2])
let mk_binop e1 op e2 =
let id = { id = op; id_loc = loc_i 2 } in
mk_expr (mk_apply_id id [e1; e2])
let mk_prefix op e1 =
let id = { id = prefix op; id_loc = loc_i 1 } in
mk_expr (mk_apply_id id [e1])
......@@ -171,8 +175,16 @@ decl:
;
lident:
| LIDENT
{ { id = $1; id_loc = loc () } }
| LIDENT { { id = $1; id_loc = loc () } }
;
uident:
| UIDENT { { id = $1; id_loc = loc () } }
;
ident:
| uident { $1 }
| lident { $1 }
;
any_op:
......@@ -181,8 +193,9 @@ any_op:
| OP3 { $1 }
;
uident:
| UIDENT { { id = $1; id_loc = loc () } }
qualid:
| ident { Qident $1 }
| uqualid DOT ident { Qdot ($1, $3) }
;
lqualid:
......@@ -199,11 +212,9 @@ expr:
| simple_expr %prec prec_simple
{ $1 }
| expr EQUAL expr
{ mk_infix $1 "=" $3 }
| expr COLONEQUAL expr
{ mk_infix $1 ":=" $3 }
{ mk_binop $1 "eq_bool" $3 }
| expr OP0 expr
{ mk_infix $1 $2 $3 }
{ mk_binop $1 ($2 ^ "_bool") $3 }
| expr OP1 expr
{ mk_infix $1 $2 $3 }
| expr OP2 expr
......@@ -212,6 +223,8 @@ expr:
{ mk_infix $1 $2 $3 }
| any_op expr %prec prefix_op
{ mk_prefix $1 $2 }
| expr COLONEQUAL expr
{ mk_infix $1 ":=" $3 }
| simple_expr list1_simple_expr %prec prec_app
{ mk_expr (mk_apply $1 $2) }
| IF expr THEN expr ELSE expr
......@@ -241,7 +254,7 @@ simple_expr:
{ mk_expr (Econstant $1) }
| BANG simple_expr
{ mk_prefix "!" $2 }
| lqualid
| qualid
{ mk_expr (Eident $1) }
| LEFTPAR expr RIGHTPAR
{ $2 }
......@@ -287,11 +300,6 @@ constant:
/*****
ident:
| uident { $1 }
| lident { $1 }
;
ident_rich:
| uident { $1 }
| lident_rich { $1 }
......
......@@ -29,6 +29,7 @@ type lazy_op = Pgm_ptree.lazy_op
type dexpr = {
dexpr_desc : dexpr_desc;
dexpr_denv : Typing.denv;
dexpr_type : Denv.dty;
dexpr_loc : loc;
}
......
......@@ -83,7 +83,8 @@ let expected_type e ty =
let rec dexpr env e =
let d, ty = expr_desc env e.Pgm_ptree.expr_loc e.Pgm_ptree.expr_desc in
{ dexpr_desc = d; dexpr_type = ty; dexpr_loc = e.Pgm_ptree.expr_loc }
{ dexpr_desc = d; dexpr_loc = e.Pgm_ptree.expr_loc;
dexpr_denv = env.denv; dexpr_type = ty; }
and expr_desc env loc = function
| Pgm_ptree.Econstant (ConstInt _ as c) ->
......@@ -130,7 +131,7 @@ and expr_desc env loc = function
let e1 = dexpr env e1 in
expected_type e1 env.ty_bool;
let e2 = dexpr env e2 in
expected_type e1 env.ty_unit;
expected_type e2 env.ty_unit;
DEwhile (e1, a, e2), env.ty_unit
| Pgm_ptree.Elazy (op, e1, e2) ->
let e1 = dexpr env e1 in
......@@ -153,12 +154,12 @@ and expr_desc env loc = function
(* phase 2: typing annotations *)
let rec expr env e =
let d = expr_desc env e.dexpr_desc in
let rec expr e =
let d = expr_desc e.dexpr_denv e.dexpr_desc in
let ty = Denv.ty_of_dty e.dexpr_type in
{ expr_desc = d; expr_type = ty; expr_loc = e.dexpr_loc }
and expr_desc env = function
and expr_desc denv = function
| DEconstant c ->
Econstant c
| DElocal x ->
......@@ -166,32 +167,39 @@ and expr_desc env = function
| DEglobal ls ->
Eglobal ls
| DEapply (e1, e2) ->
Eapply (expr env e1, expr env e2)
Eapply (expr e1, expr e2)
| DElet (x, e1, e2) ->
Elet (x, expr env e1, expr env e2)
Elet (x, expr e1, expr e2)
| DEsequence (e1, e2) ->
Esequence (expr env e1, expr env e2)
Esequence (expr e1, expr e2)
| DEif (e1, e2, e3) ->
Eif (expr env e1, expr env e2, expr env e3)
Eif (expr e1, expr e2, expr e3)
| DEwhile (e1, la, e2) ->
assert false (*TODO*)
let la =
{ loop_invariant =
option_map (Typing.type_fmla denv) la.Pgm_ptree.loop_invariant;
loop_variant =
option_map (Typing.type_term denv) la.Pgm_ptree.loop_variant; }
in
Ewhile (expr e1, la, expr e2)
| DElazy (op, e1, e2) ->
Elazy (op, expr env e1, expr env e2)
Elazy (op, expr e1, expr e2)
| DEskip ->
Eskip
| DEassert (k, f) ->
assert false (*TODO*)
let f = Typing.type_fmla denv f in
Eassert (k, f)
| DEghost e1 ->
Eghost (expr env e1)
Eghost (expr e1)
| DElabel (s, e1) ->
Elabel (s, expr env e1)
Elabel (s, expr e1)
let code uc id e =
let env = create_denv uc in
let e = dexpr env e in
ignore (expr env e)
ignore (expr e)
(*
Local Variables:
......
(* test file for ML-why *)
{
type t
logic foo : t
logic f(int) : int
logic g(x : int) : int = f(x+1)
(* Parameters.
Without loss of generality, we can take [x1=0] and [y1=0].
Thus the line to draw joins [(0,0)] to [(x2,y2)]
and we have [deltax = x2] and [deltay = y2].
Moreover we assume being in the first octant, i.e.
[0 <= y2 <= x2] (see the Coq file). The seven other cases can be easily
deduced by symmetry. *)
{
logic x2 : int
logic y2 : int
axiom First_octant : 0 <= y2 and y2 <= x2
}
let p =
let x = ref 1 in
L:
begin
assert { !x = f(1) };
ignore (!x + f 1);
g 2
end
(* Global variables of the program. *)
(* The code.
[(best x y)] expresses that the point [(x,y)] is the best
possible point i.e. the closest to the real line (see the Coq file).
The invariant relates [x], [y] and [e] and
gives lower and upper bound for [e] (see the Coq file). *)
{
use import int.Abs
let q = let x = 1 in x+2
logic best(x:int, y:int) =
forall y':int. abs (x2 * y - x * y2) <= abs (x2 * y' - x * y2)
{
axiom A : forall x:int. f(x) = g(x-1)
logic invariant(x:int, y:int, e:int) =
e = 2 * (x + 1) * y2 - (2 * y + 1) * x2 and
2 * (y2 - x2) <= e and e <= 2 * y2
lemma Invariant_is_ok : forall x,y,e:int. invariant(x,y,e) -> best(x,y)
}
let bresenham =
let x = ref 0 in
let y = ref 0 in
let e = ref (2 * y2 - x2) in
while !x <= x2 do
invariant {0 <= !x and !x <= x2 + 1 and invariant(!x, !y, !e) }
variant { x2 + 1 - !x }
(* here we would do (plot x y) *)
assert { best(!x, !y) };
if !e < 0 then
e := !e + 2 * y2
else begin
y := !y + 1;
e := !e + 2 * (y2 - x2)
end;
x := !x + 1
done
(*
Local Variables:
......
......@@ -3,14 +3,22 @@ theory Prelude
use export int.Int
use export bool.Bool
logic eq_bool('a, 'a) : bool
logic ne_bool('a, 'a) : bool
logic le_bool('a, 'a) : bool
logic lt_bool('a, 'a) : bool
logic ge_bool('a, 'a) : bool
logic gt_bool('a, 'a) : bool
use export unit.Unit
logic ignore('a) : unit
type ('a, 'b) arrow
type 'a ref
logic ref ('a) : 'a ref
logic (!_)('a ref) : 'a
use export unit.Unit
logic ignore('a) : unit
logic (:=)('a ref, 'a) : unit
type label
logic at ('a, label) : 'a
......
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