Lahenda wp praktikumis

Author: sim642

src/symbolic/symbolic.ml

@@ -58,14 +58,31 @@ let bool_of_int expr = Syntax.(expr <> ~$0)
     Vihje: let open Syntax in ...
     Vihje: int_of_bool. *)
 let eval_binary (l: Expr.expr) (b: Ast.binary) (r: Expr.expr): Expr.expr =
-  failwith "TODO"
+  let open Syntax in
+  match b with
+  | Add -> l + r
+  | Sub -> l - r
+  | Mul -> l * r
+  | Div -> l / r
+  | Mod -> l mod r
+  | Eq -> int_of_bool (l = r)
+  | Ne -> int_of_bool (l <> r)
+  | Lt -> int_of_bool (l < r)
+  | Le -> int_of_bool (l <= r)
+  | Gt -> int_of_bool (l > r)
+  | Ge -> int_of_bool (l >= r)
 
 (** Teisendab avaldise Z3 avaldiseks.
     Rand avaldist pole vaja toetada, sest see pole nii lihtne kui võib arvata.
     Vihje: let open Syntax in ...
     Vihje: eval_binary. *)
 let rec eval_expr (expr: Ast.expr): Expr.expr =
-  failwith "TODO"
+  let open Syntax in
+  match expr with
+  | Num i -> ~$i
+  | Var x -> !x
+  | Rand (l, u) -> failwith "Rand"
+  | Binary (l, b, r) -> eval_binary (eval_expr l) b (eval_expr r)
 
 
 module Env = Eval.Common.Env

src/wp/wp.ml

@@ -9,7 +9,19 @@ open Symbolic
     Vihje: Expr.substitute_one.
     Vihje: bool_of_int. *)
 let rec wp (stmt: Ast.stmt) (post: Expr.expr): Expr.expr =
-  failwith "TODO"
+  let open Syntax in
+  match stmt with
+  | Nop -> post
+  | Error -> false_
+  | Assign (x, e) ->
+    let e' = eval_expr e in
+    Expr.substitute_one post !x e'
+  | Seq (s1, s2) -> wp s1 (wp s2 post)
+  | If (c, s1, s2) ->
+    let c' = bool_of_int (eval_expr c) in
+    implies c' (wp s1 post) && implies (not c') (wp s2 post)
+  | While (Num 1, Nop) -> true_
+  | _ -> failwith "TODO"
 
 
 (** Korrektsuse kontrolli tulemus. *)
@@ -25,4 +37,8 @@ type verdict =
     Vihje: match-i Solver.check tulemust.
     Vihje: env_of_model. *)
 let check (stmt: Ast.stmt): verdict =
-  failwith "TODO"
+  let formula = Syntax.(not (wp stmt true_)) in
+  match Solver.check solver [formula] with
+  | SATISFIABLE -> Incorrect (env_of_model (Option.get (Solver.get_model solver)))
+  | UNSATISFIABLE -> Correct
+  | UNKNOWN -> Unknown