side effects of left hand side in assignment handled. Side effects like this...

side effects of left hand side in assignment handled. Side effects like this occur when assigning to arrays

Settings.hs

 module Settings where
 
 testFile, postCond :: String
-testFile = "2d-arrays1"
+testFile = "arrays1"
 postCond = "(true)"
 
 nrOfUnroll :: Int

Tests/2d-arrays1.java

+// 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

Tests/arrays1.java

+//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

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