diff --git a/Settings.hs b/Settings.hs
index 93168b614c82bd188b06a9848b3dbd9b73a79592..add915ea2d1e90ee40447cba442863e17abade2c 100644
--- a/Settings.hs
+++ b/Settings.hs
@@ -1,5 +1,5 @@
module Settings where
-testFile = "loops"
-postCond = "x == 5"
-invariant = "i <= 5"
\ No newline at end of file
+testFile = "test"
+postCond = "true"
+invariant = "true"
\ No newline at end of file
diff --git a/Tests/Test1.java b/Tests/Test1.java
deleted file mode 100644
index 1c6ad537b94e5772d9cb481a6a6bf807d4e199ef..0000000000000000000000000000000000000000
--- a/Tests/Test1.java
+++ /dev/null
@@ -1,17 +0,0 @@
-public class HelloWorld {
-
- public static void main(String[] args) {
-
- try
- {
- IOException ex;
- throw ex;
- }
- catch (IOException ex)
- {
- x = 5;
- }
-
- }
-
-}
\ No newline at end of file
diff --git a/Verifier.hs b/Verifier.hs
index 6a90896dc18d38f8ce187e550602090839c0bea5..f2d8469de6557d246ed4c3e5747df5223bc85d2a 100644
--- a/Verifier.hs
+++ b/Verifier.hs
@@ -70,11 +70,11 @@ expAssertAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQual
SuperFieldAccess id -> mkStringSymbol (prettyPrint (Name [id])) >>= mkIntVar
ClassFieldAccess (Name name) id -> mkStringSymbol (prettyPrint (Name (name ++ [id]))) >>= mkIntVar
fMethodInv invocation = case invocation of
- MethodCall (Name [Ident "length"]) [a, (Lit (Int n))] -> case a of
+ MethodCall (Name [Ident "*length"]) [a, (Lit (Int n))] -> case a of
ArrayCreate t exps dim -> foldExp expAssertAlgebra (if fromEnum n < length exps then (exps !! fromEnum n) else Lit (Int 0))
ArrayCreateInit t dim arrayInit -> mkInteger 0
- _ -> undefined
- _ -> undefined
+ _ -> error "length of non-array"
+ _ -> error (prettyPrint invocation)
fArrayAccess _ = undefined
fExpName name = do
symbol <- mkStringSymbol (prettyPrint name)
diff --git a/WLP.hs b/WLP.hs
index ab3f42056b8dad905d5495d9b49aa4ab73e33711..cb10279868add0799d7ea627a234241b9a31fca3 100644
--- a/WLP.hs
+++ b/WLP.hs
@@ -34,8 +34,10 @@ wlpStmtAlgebra :: StmtAlgebra (Inh -> Syn)
wlpStmtAlgebra = (fStmtBlock, fIfThen, fIfThenElse, fWhile, fBasicFor, fEnhancedFor, fEmpty, fExpStmt, fAssert, fSwitch, fDo, fBreak, fContinue, fReturn, fSynchronized, fThrow, fTry, fLabeled) where
fStmtBlock (Block bs) inh = foldr (\b (r, env') -> wlpBlock (inh {acc = r, env = env'}) b) (acc inh, envBlock bs (env inh)) bs -- The result of the last block-statement will be the accumulated transformer for the second-last etc. The type environment is build from the left, so it has to be done seperately.
fIfThen e s1 = fIfThenElse e s1 (const (id, [])) -- if-then is just an if-then-else with an empty else-block
- fIfThenElse e s1 s2 inh = ((\q -> (e &* fst (s1 inh) q) |* (neg e &* fst (s2 inh) q)) . acc inh, env inh)
- fWhile e s inh = ((\q -> if unsafeIsTrue (((inv &* neg e) `imp` q) &* ((inv &* e) `imp` fst (s inh) inv) &* ((inv &* e) `imp` fst (s inh {br = const q}) true)) then inv else (neg e &* q)) . acc inh, env inh)
+ fIfThenElse e s1 s2 inh = let e' = getExp (foldExp wlpExpAlgebra e) inh
+ in ((\q -> (e' &* fst (s1 inh) q) |* (neg e' &* fst (s2 inh) q)) . acc inh, env inh)
+ fWhile e s inh = let e' = getExp (foldExp wlpExpAlgebra e) inh
+ in ((\q -> if unsafeIsTrue (((inv &* neg e') `imp` q) &* ((inv &* e') `imp` fst (s inh) inv) &* ((inv &* e') `imp` fst (s inh {br = const q}) true)) then inv else (neg e' &* q)) . acc inh, env inh)
fBasicFor init me incr s inh = let loop = fst (fWhile (fromMaybeGuard me) (\inh' -> s (inh {acc = fst (wlp' inh' (incrToStmt incr))})) inh) in wlp' (inh {acc = loop}) (initToStmt init)
fEnhancedFor = error "EnhancedFor"
fEmpty inh = (acc inh, env inh) -- Empty does nothing, but still passes control to the next statement
@@ -139,10 +141,8 @@ wlpExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualIns
fQualInstanceCreation e typeArgs t args mBody inh = (QualInstanceCreation (getExp e inh) typeArgs t args mBody, (getTrans e inh, env inh))
fArrayCreate t dimLengths dim inh = (ArrayCreate t (map (flip getExp inh) dimLengths) dim, (acc inh, env inh))
fArrayCreateInit t dim init inh = (ArrayCreateInit t dim init, (acc inh, env inh))
- fFieldAccess fieldAccess inh = case fieldAccess of
- PrimaryFieldAccess e (Ident field) -> (ArrayAccess (ArrayIndex (getExp (foldExp wlpExpAlgebra e) inh) [Lit (String field)]), (acc inh, env inh))
- _ -> error "fieldaccess"
- fMethodInv = error "method call"
+ fFieldAccess fieldAccess inh = (FieldAccess fieldAccess, (acc inh, env inh))
+ fMethodInv invocation inh = (Lit Null, (acc inh, env inh))
fArrayAccess (ArrayIndex a i) inh = case catch inh of
Nothing -> (arrayAccess a i, (acc inh, env inh))
Just (cs, f) -> (arrayAccess a i, (arrayAccessWlp a i inh, env inh))
@@ -168,7 +168,7 @@ wlpExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualIns
fPreNot e inh = (PreNot $ getExp e inh, (acc inh, env inh))
fCast t e inh = (getExp e inh, (acc inh, env inh))
fBinOp e1 op e2 inh = (BinOp (getExp e1 inh) op (getExp e2 inh), (getTrans e1 (inh {acc = getTrans e2 inh}), env inh))
- fInstanceOf = error "TODO: instanceOf"
+ fInstanceOf = error "instanceOf"
fCond g e1 e2 inh = (Cond (getExp g inh) (getExp e1 inh) (getExp e2 inh), (getTrans g (inh {acc = id}) . (\q -> (getExp g inh &* getTrans e1 (inh {acc = id}) q) |* (neg (getExp g inh) &* getTrans e2 (inh {acc = id}) q)) . acc inh, env inh))
fAssign lhs op e inh = let rhs = desugarAssign lhs op (getExp e inh)
in (rhs, (substVar (env inh) (decls inh) lhs rhs . getTrans e inh, env inh))
@@ -184,7 +184,7 @@ wlpExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualIns
dimLengths a = case a of
ArrayCreate t exps dim -> exps
- _ -> map (\n -> MethodInv (MethodCall (Name [Ident "length"]) [a, (Lit (Int n))])) [0..]
+ _ -> map (\n -> MethodInv (MethodCall (Name [Ident "*length"]) [a, (Lit (Int n))])) [0..]
-- | Gets the expression attribute
getExp :: (Inh -> (Exp, Syn)) -> Inh -> Exp