diff --git a/Settings.hs b/Settings.hs
index 80effa43a609c5b59e2f115248edf4226f3f7887..0e4b16f0750287d364f51c0c7c582b23ce59ed6b 100644
--- a/Settings.hs
+++ b/Settings.hs
@@ -1,7 +1,7 @@
module Settings where
testFile, postCond :: String
-testFile = "2d-arrays1"
+testFile = "arrays1"
postCond = "(true)"
nrOfUnroll :: Int
diff --git a/Tests/2d-arrays1.java b/Tests/2d-arrays1.java
new file mode 100644
index 0000000000000000000000000000000000000000..9841c300e3ada474acea61334094e94ebbec4a42
--- /dev/null
+++ b/Tests/2d-arrays1.java
@@ -0,0 +1,87 @@
+// https://www.cs.utexas.edu/~scottm/cs307/javacode/codeSamples/Life.java
+
+import java.util.Scanner;
+
+public class Life {
+ public static void show(boolean[][] grid){
+ String s = "";
+ for(int x = 0; x < 10; x++){
+ for(int y = 0; y < 10; y++)
+ if(grid[x][y])
+ s += "*";
+ else
+ s += ".";
+ s += "\n";
+ }
+ System.out.println(s);
+ }
+
+ public static boolean[][] gen(){
+ boolean[][] grid2 = new boolean[10][10];
+ for(int r = 0; r < 10; r++)
+ {
+ for(int c = 0; c < 10; c++)
+ {
+ if( 1 > 0.7 )
+ grid2[r][c] = true;
+ }
+ }
+ return grid2;
+ }
+
+ public static void main(String[] args){
+ boolean[][] world = gen();
+ show(world);
+ System.out.println();
+ world = nextGen(world);
+ show(world);
+ Scanner sc = new Scanner(System.in);
+ while(sc.nextLine().length() == 0){
+ System.out.println();
+ world = nextGen(world);
+ show(world);
+
+ }
+ }
+
+ public static boolean[][] nextGen(boolean[][] world){
+ boolean[][] newWorld
+ = new boolean[world.length][world[0].length];
+ int num;
+ for(int w = 0; w < world.length; w++){
+ for(int l = 0; l < world[0].length; l++){
+ num = numNeighbors(world, w, l);
+ if( occupiedNext(num, world[w][l]) )
+ newWorld[w][l] = true;
+ }
+ }
+ return newWorld;
+ }
+
+ public static boolean occupiedNext(int numNeighbors, boolean occupied){
+ if( occupied && (numNeighbors == 2 || numNeighbors == 3))
+ return true;
+ else if (!occupied && numNeighbors == 3)
+ return true;
+ else
+ return false;
+ }
+
+ private static int numNeighbors(boolean[][] world, int row, int col) {
+ int num2 = world[row][col] ? -1 : 0;
+ for(int r1 = row - 1; r1 <= row + 1; r1++)
+ for(int c1 = col - 1; c1 <= col + 1; c1++)
+ if( inbounds(world, r1, c1) && world[r1][c1] )
+ num2++;
+
+ return num2;
+ }
+
+ private static boolean inbounds(boolean[][] world, int i, int c2) {
+ return i >= 0 && i < world.length && c2 >= 0 &&
+ c2 < world[0].length;
+ }
+
+
+
+}
\ No newline at end of file
diff --git a/Tests/arrays1.java b/Tests/arrays1.java
new file mode 100644
index 0000000000000000000000000000000000000000..9f0ef348a3a52d3df25870c0ca2e0953c1625d66
--- /dev/null
+++ b/Tests/arrays1.java
@@ -0,0 +1,154 @@
+//Mike Scott
+//examples of array manipulations
+
+//https://www.cs.utexas.edu/~scottm/cs307/javacode/codeSamples/ArrayExamples.java
+
+public class ArrayExamples
+{ public static void main(String[] args)
+ { int[] list = new int[7];
+
+ findAndPrintPairs(list, 5);
+ bubblesort(list);
+ /*
+ showList(list);
+
+ list = new int[11];
+ bubblesort(list);
+ showList(list);
+
+ list = new int[11];
+ bubblesort(list);
+ showList(list);
+
+ list = new int[1];
+ bubblesort(list);
+ showList(list);
+ */
+ }
+
+
+ // pre: list != null, list.length > 0
+ // post: return index of minimum element of array
+ public static int findMin(int[] list2)
+ { assert list2 != null && list2.length > 0 : "failed precondition";
+
+ int indexOfMin = 0;
+ for(int k = 1; k < list2.length; k++)
+ { if(list2[k] < list2[indexOfMin])
+ { indexOfMin = k;
+ }
+ }
+
+ return indexOfMin;
+ }
+
+
+ /*
+ *pre: list != null, newSize >= 0
+ *post: nothing. the method does not succeed it resizing the
+ * argument
+ */
+ public static void badResize(int[] list3, int newSize)
+ { assert list3 != null && newSize >= 0 : "failed precondition";
+
+ int[] temp = new int[newSize];
+ int limit = Math.min(list3.length, newSize);
+
+ for(int l = 0; l < limit; l++)
+ { temp[l] = list3[l];
+ }
+
+ // uh oh!! Changing pointer, not pointee. This breaks the
+ // relationship between the parameter and argument
+ list3 = temp;
+ }
+
+
+ /*
+ *pre: list != null, newSize >= 0
+ *post: returns an array of size newSize. Elements from 0 to newSize - 1
+ * will be copied into the new array
+ */
+ public static int[] goodResize(int[] list4, int newSize)
+ { assert list4 != null && newSize >= 0 : "failed precondition";
+
+ int[] result = new int[newSize];
+ int limit = Math.min(list4.length, newSize);
+
+ for(int m = 0; m < limit; m++)
+ { result[m] = list4[m];
+ }
+
+ return result;
+ }
+
+
+ /*
+ *pre: list != null
+ *post: prints out the indices and values of all pairs of numbers
+ *in list such that list[a] + list[b] = target
+ */
+ public static void findAndPrintPairs(int[] list5, int target)
+ { assert list5 != null : "failed precondition";
+
+ for(int i = 0; i < list5.length; i++)
+ { for(int j = i + 1; j < list5.length; j++)
+ { if(list5[i] + list5[j] == target)
+ { System.out.println("The two elements at indices " + i + " and " + j
+ + " are " + list5[i] + " and " + list5[j] + " add up to " + target);
+ }
+ }
+ }
+ }
+
+
+ /*
+ *pre: list != null;
+ *post: sort the elements of list so that they are in ascending order
+ */
+ public static void bubblesort(int[] list6)
+ {
+ assert list6 != null : "failed precondition";
+
+ int temp;
+ boolean changed = true;
+ for(int n = 0; (n < list6.length) && changed; n++)
+ { changed = false;
+ for(int o = 0; o < (list6.length - n - 1); o++)
+ { assert (o >= 0) && (o + 1 < list6.length) : "loop counter o " + o +
+ "is out of bounds.";
+ if(list6[o] > list6[o+1])
+ { changed = true;
+ temp = list6[o + 1];
+ list6[o + 1] = list6[o];
+ list6[o] = temp;
+ }
+ }
+ }
+
+ assert isAscending( list6 );
+ }
+
+
+ public static void showList(int[] list7)
+ { for(int p = 0; p < list7.length; p++)
+ System.out.print( list7[p] + " " );
+ System.out.println();
+ }
+
+ /* pre: list != null
+ post: return true if list is sorted in ascedning order, false otherwise
+ */
+ public static boolean isAscending( int[] list8 )
+ { boolean ascending = true;
+ int index = 1;
+ while( ascending && (index < list8.length) )
+ { assert (index >= 0) && (index < list8.length);
+
+ ascending = (list8[index - 1] <= list8[index]);
+ index++;
+ }
+
+ return ascending;
+ }
+}
\ No newline at end of file
diff --git a/WLP.hs b/WLP.hs
index 89327e592cdb2e096b7ff6213bce0cac70f12873..83bb0526affaad6358c259f8efabfe519d5769da 100644
--- a/WLP.hs
+++ b/WLP.hs
@@ -46,14 +46,14 @@ wlpStmtAlgebra = (fStmtBlock, fIfThen, fIfThenElse, fWhile, fBasicFor, fEnhanced
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
- fAssert e _ inh = let (e', trans) = foldExp wlpExpAlgebra e inh
- in ((e' &*) . trans)
+ fAssert e _ inh = let (e', trans) = foldExp wlpExpAlgebra e inh {acc = id}
+ in (trans . (e' &*) . acc inh)
fSwitch e bs inh = let (e', s1, s2) = desugarSwitch e bs in fIfThenElse e' (flip wlp' s1) (flip wlp' s2) (inh {acc = id, br = acc inh})
fDo s e inh = s (inh {acc = fWhile e s inh}) -- Do is just a while with the statement block executed one additional time. Break and continue still have to be handled in this additional execution.
- fBreak _ inh = (br inh) -- wlp of the breakpoint. Control is passed to the statement after the loop
- fContinue _ inh = (id) -- at a continue statement it's as if the body of the loop is fully executed
+ fBreak _ inh = br inh -- wlp of the breakpoint. Control is passed to the statement after the loop
+ fContinue _ inh = id -- at a continue statement it's as if the body of the loop is fully executed
fReturn me inh = case me of
- Nothing -> (id) -- Return ignores acc, as it terminates the method
+ Nothing -> id -- Return ignores acc, as it terminates the method
Just e -> fExpStmt (Assign (NameLhs (Name [fromJust' "fReturn" (ret inh)])) EqualA e) (inh {acc = id}) -- We treat "return e" as an assignment to a variable specifically created to store the return value in
fSynchronized _ = fStmtBlock
@@ -170,7 +170,7 @@ wlpExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualIns
in (ExpName (Name [varId]), (callWlp . acc inh))
fArrayAccess (ArrayIndex a i) inh = (arrayAccess a i, snd ((foldExp wlpExpAlgebra a) inh {acc = id}) . arrayAccessWlp a i inh)
- fExpName name inh = (ExpName name, (acc inh))
+ fExpName name inh = (editName inh name, acc inh)
-- x++ increments x but evaluates to the original value
fPostIncrement e inh = let (e', trans) = e inh in
case e' of
@@ -203,12 +203,9 @@ wlpExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualIns
(e2', trans2) = e2 inh {acc = id}
(g', transg) = g inh {acc = id}
in (Cond g' e1' e2', (transg . (\q -> (g' &* trans1 q) |* (neg g' &* trans2 q)) . acc inh))
- fAssign lhs op e inh = let lhs' = foldLhs inh lhs
+ fAssign lhs op e inh = let (lhs', lhsTrans) = foldLhs inh {acc = id} lhs
rhs' = desugarAssign lhs' op e'
(e', trans) = e inh {acc = id}
- lhsTrans = case lhs' of
- ArrayLhs (ArrayIndex a i) -> arrayAccessWlp a i inh {acc = id}
- _ -> id
in (rhs', lhsTrans . trans . substVar (env inh) (decls inh) lhs' rhs' . acc inh)
fLambda = error "lambda"
fMethodRef = error "method reference"
@@ -224,6 +221,13 @@ wlpExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualIns
ArrayCreate t exps dim -> exps
_ -> map (\n -> MethodInv (MethodCall (Name [Ident "*length"]) [a, (Lit (Int n))])) [0..]
+ -- Edits a name expression to handle build-in constructs
+ editName :: Inh -> Name -> Exp
+ editName inh (Name name) | last name == Ident "length" = case lookupType (decls inh) (env inh) (Name (take (length name - 1) name)) of -- For arrays we know that "length" refers to the length of the array
+ RefType (ArrayType _) -> MethodInv (MethodCall (Name [Ident "*length"]) [ExpName (Name (take (length name - 1) name)), (Lit (Int 0))])
+ _ -> ExpName (Name name)
+ | otherwise = ExpName (Name name)
+
-- Inlines a methodcall. This creates a variable to store the return value in
inlineMethod :: Inh -> MethodInvocation -> Stmt
inlineMethod inh invocation = StmtBlock (Block (getParams inh invocation ++ [BlockStmt (getBody inh invocation)])) where
@@ -267,14 +271,15 @@ wlpExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualIns
getType inh invocation = getMethodType (decls inh) (invocationToId invocation)
-- Folds the expression part of an lhs
- foldLhs :: Inh -> Lhs -> Lhs
+ foldLhs :: Inh -> Lhs -> (Lhs, Syn)
foldLhs inh lhs = case lhs of
- FieldLhs (PrimaryFieldAccess e id) -> case fst (foldExp wlpExpAlgebra e inh) of
- ExpName name -> NameLhs (Name (fromName name ++ [id]))
- _ -> error "foldFieldAccess"
- ArrayLhs (ArrayIndex e i) -> let e' = fst (foldExp wlpExpAlgebra e inh)
- in ArrayLhs (ArrayIndex e' (map (\e'' -> fst (foldExp wlpExpAlgebra e'' inh)) i))
- lhs' -> lhs'
+ FieldLhs (PrimaryFieldAccess e id) -> case foldExp wlpExpAlgebra e inh of
+ (ExpName name, trans) -> (NameLhs (Name (fromName name ++ [id])), trans)
+ _ -> error "foldFieldAccess"
+ ArrayLhs (ArrayIndex a i) -> let (a', aTrans) = foldExp wlpExpAlgebra a inh
+ i' = map (\x -> foldExp wlpExpAlgebra x inh) i
+ in (ArrayLhs (ArrayIndex a' (map fst i')), foldl (\trans (_, iTrans) -> trans . iTrans) aTrans i' . arrayAccessWlp a' (map fst i') inh)
+ lhs' -> (lhs', id)
-- Folds the expression part of a fieldaccess and simplifies it to a name
foldFieldAccess :: Inh -> FieldAccess -> Name