From 952b56adf2e03e378df4c0b853f33118c9b4a75b Mon Sep 17 00:00:00 2001
From: koen <koenwermer@gmail.com>
Date: Wed, 14 Sep 2016 01:33:53 +0200
Subject: [PATCH] fbreak and fwhile added
---
Verifier.hs | 6 ++++++
WLP.hs | 33 +++++++++++++++++++++------------
2 files changed, 27 insertions(+), 12 deletions(-)
create mode 100644 Verifier.hs
diff --git a/Verifier.hs b/Verifier.hs
new file mode 100644
index 0000000..ba74ca1
--- /dev/null
+++ b/Verifier.hs
@@ -0,0 +1,6 @@
+module Verifier where
+
+import Language.Java.Syntax
+
+isTrue :: Exp -> Bool
+isTrue = undefined
\ No newline at end of file
diff --git a/WLP.hs b/WLP.hs
index d4956b7..f52c836 100644
--- a/WLP.hs
+++ b/WLP.hs
@@ -4,6 +4,8 @@ import Language.Java.Syntax
import Language.Java.Lexer
import Language.Java.Parser
+import Verifier
+
type StmtAlgebra r = (Block -> r,
@@ -55,20 +57,22 @@ foldStmt (fStmtBlock, fIfThen, fIfThenElse, fWhile, fBasicFor, fEnhancedFor, fEm
_ -> error "TODO: complete foldStmt cases"
-- | The algebra that defines the wlp transformer for statements
-wlpStmtAlgebra :: StmtAlgebra (Exp -> Exp)
+-- The synthesized attribute is the resulting transformer.
+-- The inherited attribute represent the accumulated transformer up till the last block (this is used when handling break statements etc.)
+wlpStmtAlgebra :: StmtAlgebra ((Exp -> Exp) -> (Exp -> Exp))
wlpStmtAlgebra = (fStmtBlock, fIfThen, fIfThenElse, fWhile, fBasicFor, fEnhancedFor, fEmpty, fExpStmt, fAssert, fSwitch, fDo, fBreak, fContinue, fReturn, fSynchronized, fThrow, fTry, fLabeled) where
- fStmtBlock (Block bs) = foldr ((.) . wlpBlock) id bs
- fIfThen e s1 = fIfThenElse e s1 id
- fIfThenElse e s1 s2 = (\q -> (e &* s1 q) |* (neg e &* s2 q))
- fWhile = undefined
+ fStmtBlock (Block bs) inh = let x = foldr ((.) . wlpBlock x) id bs in x
+ fIfThen e s1 = fIfThenElse e s1 (const id)
+ fIfThenElse e s1 s2 inh = (\q -> (e &* (s1 inh) q) |* (neg e &* (s2 inh) q))
+ fWhile e s inh = (\q -> if isTrue ((inv &* neg e) `imp` q) then inv else (neg e &* q)) -- We assume the given invariant is correct
fBasicFor = undefined
fEnhancedFor = undefined
- fEmpty = id
+ fEmpty inh = id
fExpStmt = undefined
fAssert = undefined
fSwitch = undefined
fDo = undefined
- fBreak = undefined
+ fBreak _ inh = inh
fContinue = undefined
fReturn = undefined
fSynchronized = undefined
@@ -76,13 +80,18 @@ wlpStmtAlgebra = (fStmtBlock, fIfThen, fIfThenElse, fWhile, fBasicFor, fEnhanced
fTry = undefined
fLabeled = undefined
-- Helper functions
- wlpBlock b = case b of
- BlockStmt s -> wlp s
- LocalClass _ -> id
- LocalVars mods t vars -> undefined
+ wlpBlock inh b = case b of
+ BlockStmt s -> wlp' inh s
+ LocalClass _ -> id
+ LocalVars mods t vars -> undefined
+ inv = Lit (Boolean True) -- for simplicity, "True" is used as an invariant for now
-- | Calculates the weakest liberal pre-condition of a statement and a given post-condition
wlp :: Stmt -> Exp -> Exp
-wlp = foldStmt wlpStmtAlgebra
+wlp = wlp' id
+
+-- wlp' lets you specify the inherited attribute
+wlp' :: (Exp -> Exp) -> Stmt -> Exp -> Exp
+wlp' inh s = foldStmt wlpStmtAlgebra s inh
--
GitLab