From 96fb04377e3538996a3895c2a97c6b1efa5c60c2 Mon Sep 17 00:00:00 2001
From: koen <koenwermer@gmail.com>
Date: Tue, 3 Jan 2017 17:04:06 +0100
Subject: [PATCH] more array examples
---
Settings.hs | 2 +-
Tests/arrays2.java | 31 +++++++++++++++++++++++++++++++
Tests/arrays3.java | 43 +++++++++++++++++++++++++++++++++++++++++++
WLP.hs | 3 ++-
4 files changed, 77 insertions(+), 2 deletions(-)
create mode 100644 Tests/arrays2.java
create mode 100644 Tests/arrays3.java
diff --git a/Settings.hs b/Settings.hs
index 0e4b16f..0653c92 100644
--- a/Settings.hs
+++ b/Settings.hs
@@ -1,7 +1,7 @@
module Settings where
testFile, postCond :: String
-testFile = "arrays1"
+testFile = "arrays3"
postCond = "(true)"
nrOfUnroll :: Int
diff --git a/Tests/arrays2.java b/Tests/arrays2.java
new file mode 100644
index 0000000..bb9bf88
--- /dev/null
+++ b/Tests/arrays2.java
@@ -0,0 +1,31 @@
+//https://www.tutorialspoint.com/java/java_arrays.htm
+
+public class TestArray {
+
+ public static void main(String[] args) {
+ double[] myList = new double[4];
+ myList[0] = 1.9;
+ myList[1] = 2.9;
+ myList[2] = 3.4;
+ myList[3] = 3.5;
+
+ // Print all the array elements
+ for (int i = 0; i < myList.length; i++) {
+ System.out.println(myList[i] + " ");
+ }
+
+ // Summing all elements
+ double total = 0;
+ for (int j = 0; j < myList.length; j++) {
+ total += myList[j];
+ }
+ System.out.println("Total is " + total);
+
+ // Finding the largest element
+ double max = myList[0];
+ for (int k = 1; k < myList.length; k++) {
+ if (myList[k] > max) max = myList[k];
+ }
+ System.out.println("Max is " + max);
+ }
+}
\ No newline at end of file
diff --git a/Tests/arrays3.java b/Tests/arrays3.java
new file mode 100644
index 0000000..212a200
--- /dev/null
+++ b/Tests/arrays3.java
@@ -0,0 +1,43 @@
+//https://examples.javacodegeeks.com/java-basics/arrays-java-basics/java-string-array-example/
+
+package com.javacodegeeks.javabasics.stringarray;
+
+public class JavaStringArrayExample {
+
+ public static void main(String args[]) {
+
+ // declare a string array with initial size
+ String[] schoolbag = new String[4];
+
+ // add elements to the array
+ schoolbag[0] = "Books";
+ schoolbag[1] = "Pens";
+ schoolbag[2] = "Pencils";
+ schoolbag[3] = "Notebooks";
+
+ // this will cause ArrayIndexOutOfBoundsException
+ // schoolbag[4] = "Notebooks";
+
+ // declare a string array with no initial size
+ // String[] schoolbag;
+
+ // declare string array and initialize with values in one step
+ String[] schoolbag2 = new String[4];
+ schoolbag2[0] = "Books";
+ schoolbag2[1] = "Pens";
+ schoolbag2[2] = "Pencils";
+ schoolbag2[3] = "Notebooks";
+
+ // print the third element of the string array
+ System.out.println("The third element is: " + schoolbag2[2]);
+
+ // iterate all the elements of the array
+ int size = schoolbag2.length;
+ System.out.println("The size of array is: " + size);
+ for (int i = 0; i < size; i++) {
+ System.out.println("Index[" + i + "] = " + schoolbag2[i]);
+ }
+
+ }
+
+}
\ No newline at end of file
diff --git a/WLP.hs b/WLP.hs
index 83bb052..316898a 100644
--- a/WLP.hs
+++ b/WLP.hs
@@ -87,6 +87,7 @@ wlpStmtAlgebra = (fStmtBlock, fIfThen, fIfThenElse, fWhile, fBasicFor, fEnhanced
-- We don't initialize ref types to null, because we want to keep pointer information
RefType _ -> acc inh
wlpDeclAssignment t inh (VarDecl (VarId ident) (Just (InitExp e))) = snd (foldExp wlpExpAlgebra (Assign (NameLhs (Name [ident])) EqualA e) inh)
+ wlpDeclAssignment _ _ _ = error "ArrayCreateInit is not supported"
-- Unrolls a while-loop a finite amount of times
unrollLoop :: Inh -> Int -> Exp -> (Exp -> Exp) -> (Exp -> Exp) -> Exp -> Exp
@@ -159,7 +160,7 @@ wlpExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualIns
in (ExpName var, (substVar (env inh) (decls inh) (NameLhs var) (InstanceCreation typeArgs t [ExpName (Name [Ident "#"])] mBody) . snd ((fMethodInv invocation) inh {acc = id}) . acc inh))
fQualInstanceCreation e typeArgs t args mBody inh = error "fQualInstanceCreation"
fArrayCreate t dimLengths dim inh = (ArrayCreate t (map (\e -> fst (e inh)) dimLengths) dim, acc inh)
- fArrayCreateInit t dim init inh = (ArrayCreateInit t dim init, acc inh)
+ fArrayCreateInit t dim init inh = error "ArrayCreateInit" -- (ArrayCreateInit t dim init, acc inh)
fFieldAccess fieldAccess inh = (ExpName (foldFieldAccess inh fieldAccess), (acc inh))
fMethodInv invocation inh = case invocation of
MethodCall (Name [Ident "*assume"]) [e] -> (false, (if e == false then const true else imp e)) -- *assume is the regular assume function
--
GitLab