added weakest precondition of assignment and fixed domain

Author: lamg

Prover/LanguageServices/Wybe/Semantics.fs

@@ -82,15 +82,25 @@ let rec checkChildrenFixedType
     | _ -> None)
   |> List.choose id
   |> function
-    | [] -> ST((Typed resultType, e), xs)
+    | [] ->
+      let childrenDomains = xs |> List.choose (fun x -> x.SemanticResult.Domain)
+
+      match childrenDomains with
+      | [] -> ST((Typed resultType, e), xs)
+      | _ -> ST((TypedDomain(resultType, childrenDomains), e), xs)
+
     | rs -> ST((Expecting rs, e), xs)
 
 and checkChildrenEqualType (vars: Map<string, Type>) (e: Expr, resultType: Type) (children: Expr list) =
   let xs = children |> List.map (extractTypeAndDomain vars)
   let types = xs |> List.choose _.SemanticResult.Type |> Set
 
   if Set.count types = 1 then
-    ST((Typed resultType, e), xs)
+    let childrenDomains = xs |> List.choose (fun x -> x.SemanticResult.Domain)
+
+    match childrenDomains with
+    | [] -> ST((Typed resultType, e), xs)
+    | _ -> ST((TypedDomain(resultType, childrenDomains), e), xs)
   else
     ST((ExpectingSameType(Set.toList types), e), xs)
 
@@ -106,8 +116,12 @@ and extractTypeAndDomain (vars: Map<string, Type>) (e: Expr) : SemanticTree =
       let r =
         checkChildrenFixedType vars (e, Type.Integer) (Type.Integer, [ left; right ])
 
-      let divDomain = Binary(right, Op.Differs, Lit(Int 0)) |> extractTypeAndDomain vars
-      r.AddDomain divDomain
+      let zero = Lit(Int 0)
+      let diffZero = Binary(right, Op.Differs, zero)
+      let typedZero = ST((Typed Type.Integer, zero), [])
+
+      let domain = ST((Typed Type.Boolean, diffZero), [ r.Children[1]; typedZero ])
+      r.AddDomain domain
     | Op.Equals
     | Op.Differs -> checkChildrenEqualType vars (e, Type.Boolean) [ left; right ]
     | Op.AtMost
@@ -400,7 +414,7 @@ let semanticExprToWExpr (e: SemanticTree) : DomainWExpr option =
         | None -> None
       | Lit(Bool b), [] -> Some(if b then True else False)
       | Expr.Var name, [] -> Some(mkBoolVar name)
-      | _ -> failwith $"not implemented: {exprToTree e.Expr}"
+      | _ -> failwith $"unexpected boolean expression: {exprToTree e.Expr}"
     | Some Type.Integer ->
       match e.Expr, e.Children with
       | Lit(Int i), [] -> Some(Integer i)
@@ -475,3 +489,28 @@ let semanticExprToWExpr (e: SemanticTree) : DomainWExpr option =
 
   let domain = e.SemanticResult.Domain |> Option.bind typedToWExpr
   typedToWExpr e |> Option.map (fun r -> DomainWExpr(domain, r))
+
+// weakest precondition of assignemt
+let wpAssignment (vars: Map<string, Type>, var: string, expr: Expr, postcondition: Expr) =
+  let rec loop (target: Expr) =
+    match target with
+    | Expr.Var name when name.Equals var -> expr
+    | Binary(l, op, r) -> Binary(loop l, op, loop r)
+    | Unary(op, r) -> Unary(op, loop r)
+    | Array xs -> Array(xs |> List.map loop)
+    | ArrayElem(name, index) -> ArrayElem(name, loop index)
+    | _ -> target
+
+  match extractTypeAndDomain vars postcondition with
+  | postconditionST when postconditionST.SemanticResult.Type.Equals(Some Type.Boolean) ->
+    let exprSubstituted = loop postcondition
+
+    match extractTypeAndDomain vars exprSubstituted with
+    | substituted when substituted.SemanticResult.Type.Equals(Some Type.Boolean) ->
+
+      match semanticExprToWExpr substituted with
+      | Some wexpr when wexpr.Domain.IsSome -> Some(wexpr.Domain.Value <&&> wexpr.Expr)
+      | Some wexpr -> Some(wexpr.Expr :?> Proposition)
+      | _ -> None
+    | _ -> None
+  | _ -> None

Test/WybeLangTest.fs

@@ -74,34 +74,23 @@ let ``domain conjunction`` () =
     [ "xs", Type.Array Type.Integer; "i", Type.Integer; "j", Type.Integer ]
     |> Map.ofList
 
-  let indexExpr = Binary(Var "i", Op.Div, Var "j")
-  let r = extractTypeAndDomain vars (ArrayElem("xs", indexExpr))
-  shouldEqual "xs[ i ÷ j ]" (r.Expr |> exprToTree |> string)
-  shouldEqual (Some Type.Integer) r.SemanticResult.Type
-
-  let arrayDomain =
-    Binary(Binary(Lit(Int 0), Op.AtMost, indexExpr), Op.And, Binary(indexExpr, Op.LessThan, Unary(Op.Length, Var "xs")))
-
-  let divDomain = Binary(Var "j", Op.Differs, Lit(Int 0))
-
-  let expectedDomain =
-    Binary(divDomain, Op.And, arrayDomain)
-    |> extractTypeAndDomain vars
-    |> _.Expr
-    |> exprToTree
-    |> string
+  let iDivJ = Binary(Var "i", Op.Div, Var "j")
 
-  shouldEqual "j ≠ 0 ∧ 0 ≤ i ÷ j ∧ i ÷ j < #xs" expectedDomain
-  let actualDomain = exprToTree (r.SemanticResult.Domain.Value.Expr) |> string
+  [ ArrayElem("xs", iDivJ), (Some Type.Integer), "xs[ i ÷ j ]", "j ≠ 0 ∧ 0 ≤ i ÷ j ∧ i ÷ j < #xs"
+    Binary(iDivJ, Op.Exceeds, Lit(Int 0)), (Some Type.Boolean), "i ÷ j > 0", "j ≠ 0" ]
+  |> List.iter (fun (expr, expectedType, representation, domain) ->
+    let r = extractTypeAndDomain vars expr
+    shouldEqual representation (r.Expr |> exprToTree |> string)
+    shouldEqual expectedType r.SemanticResult.Type
+    Assert.True(r.SemanticResult.Domain.IsSome, $"No domain at {representation}")
+    let actualDomain = exprToTree (r.SemanticResult.Domain.Value.Expr) |> string
 
-  shouldEqual expectedDomain actualDomain
+    shouldEqual domain actualDomain)
 
 open GriesSchneider
 
 [<Fact>]
 let ``Expr to WExpr`` () =
-  let x, y = mkBoolVar "x", mkBoolVar "y"
-  let n, m = mkIntVar "n", mkIntVar "m"
 
   let vars =
     [ "n", Type.Integer; "m", Type.Integer; "x", Type.Boolean; "y", Type.Boolean ]
@@ -114,3 +103,17 @@ let ``Expr to WExpr`` () =
     let r = semanticExprToWExpr e
     Assert.True(r.IsSome, $"{collectSemanticTreeInfo e}")
     shouldEqual expected r.Value.Expr)
+
+[<Fact>]
+let ``weakest precondition assignment`` () =
+  let vars =
+    [ "n", Type.Integer; "m", Type.Integer; "x", Type.Boolean; "y", Type.Boolean ]
+    |> Map.ofList
+
+  let nExceeds0 = Binary(Expr.Var "n", Op.Exceeds, Lit(Int 0))
+
+  [ "n", Binary(Expr.Var "n", Op.Plus, Lit(Int 1)), nExceeds0, Some(n + 1 > zero)
+    "n", Binary(Expr.Var "n", Op.Div, Expr.Var "m"), nExceeds0, Some(m != zero <&&> (n / m > zero)) ]
+  |> List.iter (fun (var, expr, postcondition, wp) ->
+    let r = wpAssignment (vars, var, expr, postcondition)
+    shouldEqual wp r)