Lisa wp

Author: sim642

src/wp/dune

@@ -0,0 +1,4 @@
+(library
+ (name wp)
+ (libraries ast eval symbolic z3)
+ (preprocess (pps ppx_deriving.std)))

src/wp/wp.ml

@@ -0,0 +1,28 @@
+(** Nõrgima eeltingimuse arvutamine ja sellega programmi korrektsuse kontrollimine. *)
+open Z3
+open Symbolic
+
+(** Arvutab lause nõrgima eeltingimuse antud järeltingimuse jaoks.
+    Üldist While lauset pole vaja toetada, ainult piisavalt, et testid läbi läheks.
+    Vihje: let open Syntax in ...
+    Vihje: eval_expr.
+    Vihje: Expr.substitute_one.
+    Vihje: bool_of_int. *)
+let rec wp (stmt: Ast.stmt) (post: Expr.expr): Expr.expr =
+  failwith "TODO"
+
+
+(** Korrektsuse kontrolli tulemus. *)
+type verdict =
+  | Correct (** Korrektne ehk Error lauset ei täideta. *)
+  | Incorrect of Env.t (** Vigane ehk Error lauset täidetakse. Andmetena kaasas keskkond, milles Error lauseni jõutakse. *)
+  | Unknown (** Z3 ei oska lahendada. *)
+[@@deriving show]
+
+(** Kontrollib, kas programm on korrektne.
+    Vt. Toyatp.Bool.check.
+    Vihje: wp.
+    Vihje: match-i Solver.check tulemust.
+    Vihje: env_of_model. *)
+let check (stmt: Ast.stmt): verdict =
+  failwith "TODO"

test/wp/dune

@@ -0,0 +1,3 @@
+(test
+ (name wp_test)
+ (libraries ounit2 ounittodo ast eval symbolic wp))