Commit 1c9b0065 authored by Maxime Folschette's avatar Maxime Folschette
Browse files

add set and assert intructions

parent 4b705bc4
......@@ -692,25 +692,26 @@ struct
(** Grammaire des programmes impératifs *)
type prog =
| Skip
(* | Set of BRN.var * int *) (* TODO: Instruction Set (knockdown) ? *)
| Set of BRN.var * int (* TODO: Instruction Set (knockdown) *)
| Incr of BRN.var
| Decr of BRN.var
| Seq of prog * prog
| If of FOL.formula * prog * prog
| While of FOL.formula * FOL.formula * prog
| Forall of prog * prog
| Exists of prog * prog ;;
(* | Assert of FOL.formula *) (* TODO: Instruction Assert ? *)
| Exists of prog * prog
| Assert of FOL.formula ;; (* TODO: Instruction Assert *)
(** Conversion d'un programme impératif en chaîne de caractères pour affichage avec indentations *)
let string_of_prog_indent p =
let nli indent = ("\n" ^ (String.make indent ' ')) in
let newindent = 2 in
let rec string_of_prog_indentation p indent =
(match p with
match p with
| Skip -> "SKIP"
| Incr(v) -> ((BRN.string_of_var v) ^ "++")
| Decr(v) -> ((BRN.string_of_var v) ^ "−−")
| Incr(v) -> ((BRN.string_of_var v) ^ "+")
| Decr(v) -> ((BRN.string_of_var v) ^ "−")
| Set(v, k) -> ((BRN.string_of_var v) ^ " := " ^ (string_of_int k))
| Seq(p1, p2) -> ((string_of_prog_indentation p1 indent) ^ " ;"
^ (nli indent) ^ (string_of_prog_indentation p2 indent))
| If(c, p1, p2) -> ("IF " ^ (FOL.string_of_formula c) ^ " THEN"
......@@ -722,19 +723,22 @@ struct
^ (nli (indent + newindent)) ^ (string_of_prog_indentation p (indent + newindent))
^ (nli indent) ^ "END WHILE")
| Forall(p1, p2) -> ("∀(" ^ (string_of_prog_indentation p1 indent) ^ ", " ^ (string_of_prog_indentation p2 indent) ^ ")")
| Exists(p1, p2) -> ("∃(" ^ (string_of_prog_indentation p1 indent) ^ ", " ^ (string_of_prog_indentation p2 indent) ^ ")")) in
| Exists(p1, p2) -> ("∃(" ^ (string_of_prog_indentation p1 indent) ^ ", " ^ (string_of_prog_indentation p2 indent) ^ ")")
| Assert(f) -> ("assert(" ^ (FOL.string_of_formula f) ^ ")") in
string_of_prog_indentation p 0 ;;
(** Conversion d'un programme impératif en chaîne de caractères pour affichage en ligne *)
let rec string_of_prog = function
| Skip -> "SKIP"
| Incr(v) -> ((BRN.string_of_var v) ^ "++")
| Decr(v) -> ((BRN.string_of_var v) ^ "−−")
| Incr(v) -> ((BRN.string_of_var v) ^ "+")
| Decr(v) -> ((BRN.string_of_var v) ^ "−")
| Set(v, k) -> ((BRN.string_of_var v) ^ " := " ^ (string_of_int k))
| Seq(p1, p2) -> ((string_of_prog p1) ^ " ; " ^ (string_of_prog p2))
| If(c, p1, p2) -> ("(IF " ^ (FOL.string_of_formula c) ^ " THEN " ^ (string_of_prog p1) ^ " ELSE " ^ (string_of_prog p2) ^ " END IF)")
| While(c, i, p) -> ("(WHILE " ^ (FOL.string_of_formula c) ^ " WITH " ^ (FOL.string_of_formula i) ^ " DO " ^ (string_of_prog p) ^ " END WHILE)")
| Forall(p1, p2) -> ("∀(" ^ (string_of_prog p1) ^ ", " ^ (string_of_prog p2) ^ ")")
| Exists(p1, p2) -> ("∃(" ^ (string_of_prog p1) ^ ", " ^ (string_of_prog p2) ^ ")") ;;
| Exists(p1, p2) -> ("∃(" ^ (string_of_prog p1) ^ ", " ^ (string_of_prog p2) ^ ")")
| Assert(f) -> ("assert(" ^ (FOL.string_of_formula f) ^ ")") ;;
end ;;
......@@ -785,13 +789,15 @@ struct
| Skip -> post
| Incr v -> PropBin(And, phi_incr v, replace post v (incr_formula v))
| Decr v -> PropBin(And, phi_decr v, replace post v (decr_formula v))
| Seq (p1, p2) -> wp p1 (wp p2 post)
| If (c, p1, p2) -> PropBin(And, PropBin(Impl, c, wp p1 post),
| Set(v, k) -> replace post v (ExprConst(k))
| Seq(p1, p2) -> wp p1 (wp p2 post)
| If(c, p1, p2) -> PropBin(And, PropBin(Impl, c, wp p1 post),
PropBin(Impl, PropUn(Neg, c), wp p2 post))
| While (c, i, p) -> PropBin(And, i, PropBin(And, FreshState(PropBin(Impl, PropBin(And, i, c), wp p i)),
| While(c, i, p) -> PropBin(And, i, PropBin(And, FreshState(PropBin(Impl, PropBin(And, i, c), wp p i)),
FreshState(PropBin(Impl, PropBin(And, i, PropUn(Neg, c)), post))))
| Forall (p1, p2) -> PropBin(And, wp p1 post, wp p2 post)
| Exists (p1, p2) -> PropBin(Or, wp p1 post, wp p2 post) ;;
| Forall(p1, p2) -> PropBin(And, wp p1 post, wp p2 post)
| Exists(p1, p2) -> PropBin(Or, wp p1 post, wp p2 post)
| Assert(f) -> PropBin(And, f, post) ;;
end ;;
......@@ -1078,6 +1084,21 @@ print_endline (string_of_formula pre4b) ;;
write_example pre4b "simpleex4b.lp" ;;
(* OK : Aucune solution (avec raffinage) *)
let prog5 = Seq(Seq(Seq(Incr B, Set(C, 1)), Assert(PropBin(And, Rel(Eq, ExprVar(B), ExprConst(1)), Rel(Eq, ExprVar(A), ExprConst(1))))), Decr B) ;;
let post5 = PropConst True ;;
(* let pre4b = wp prog4b post4b ;; (* Sans raffinage *) *)
let pre5 = and_simplify (wp prog5 post5) [(* (A, 1) ; *) (B, 0) ; (C, 0)] [] ;; (* Avec raffinage et simplification *)
print_endline "***************************************************" ;;
print_endline "*** Exemple 5 : Tests simples sur Set et Assert ***" ;;
print_endline "***************************************************" ;;
print_endline "*** Programme ***" ;;
print_endline (string_of_prog_indent prog5) ;;
print_endline "*** Post-condition ***" ;;
print_endline (string_of_formula post5) ;;
print_endline "*** Plus faible pré-condition simplifiée ***" ;;
print_endline (string_of_formula pre5) ;;
write_example pre5 "simpleex5.lp" ;;
(** Phage lambda (depuis la thèse d'Adrien Richard) *)
......
Supports Markdown
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