From 7646a01d6fd091e5b0338107a54a24885b0f76ab Mon Sep 17 00:00:00 2001
From: ISWB Prasetya <iswbprasetya@iswbs-mbp.cs.uu.nl>
Date: Wed, 4 Jan 2017 15:54:34 +0100
Subject: [PATCH] bug fixing WLP
---
WLP.hs | 4 ++--
1 file changed, 2 insertions(+), 2 deletions(-)
diff --git a/WLP.hs b/WLP.hs
index 316898a..8ebf692 100644
--- a/WLP.hs
+++ b/WLP.hs
@@ -42,7 +42,7 @@ wlpStmtAlgebra = (fStmtBlock, fIfThen, fIfThenElse, fWhile, fBasicFor, fEnhanced
fWhile e s inh = let (e', trans) = foldExp wlpExpAlgebra e inh {acc = id}
var = getVar
in (\q -> unrollLoop inh nrOfUnroll e' trans (s (inh {acc = id, br = const q})) q) . acc inh
- fBasicFor init me incr s inh = let loop = (fWhile (fromMaybeGuard me) (\inh' -> s (inh {acc = (wlp' inh {acc = id} (incrToStmt incr))})) inh) in wlp' (inh {acc = loop}) (initToStmt init)
+ fBasicFor init me incr s inh = let loop = (fWhile (fromMaybeGuard me) (\inh' -> s (inh' {acc = (wlp' inh' {acc = id} (incrToStmt incr))})) inh) in wlp' (inh {acc = loop}) (initToStmt init)
fEnhancedFor = error "EnhancedFor"
fEmpty inh = (acc inh) -- Empty does nothing, but still passes control to the next statement
fExpStmt e inh = snd $ foldExp wlpExpAlgebra e inh
@@ -94,7 +94,7 @@ wlpStmtAlgebra = (fStmtBlock, fIfThen, fIfThenElse, fWhile, fBasicFor, fEnhanced
unrollLoop inh 0 g gTrans _ = let var = getVar
in gTrans . substVar' inh var g . (neg (ExpName (Name [var])) `imp`)
unrollLoop inh n g gTrans bodyTrans = let var = getVar
- in gTrans . substVar' inh var g . (\q -> (ExpName (Name [var]) &* bodyTrans q) |* (neg (ExpName (Name [var])) &* unrollLoop inh (n-1) g gTrans bodyTrans q))
+ in gTrans . substVar' inh var g . (\q -> (neg (ExpName (Name [var])) `imp` q) &* ((ExpName (Name [var])) `imp` bodyTrans (unrollLoop inh (n-1) g gTrans bodyTrans q)))
-- Converts initialization code of a for loop to a statement
--
GitLab