From b818715be678fc30cb30a5a48d550fbc728eb408 Mon Sep 17 00:00:00 2001
From: ISWB Prasetya <iswbprasetya@iswbs-mbp.cs.uu.nl>
Date: Tue, 22 Aug 2017 13:57:03 +0200
Subject: [PATCH] fixing the small examples
---
examples/2d-arrays1.java | 87 ---------------------------------
examples/arrays.java | 19 -------
examples/arrays1.java | 2 +-
examples/arrays2.java | 4 +-
examples/arrays3.java | 6 +--
examples/loops.java | 14 ++----
examples/methods.java | 66 ++++++++++---------------
examples/objects.java | 31 +++++-------
examples/side-effects.java | 27 ----------
examples/simple.java | 6 +--
examples/switch.java | 5 +-
examples/try-catch-finally.java | 38 --------------
src/Javawlp/Engine/WLP.hs | 11 ++++-
13 files changed, 65 insertions(+), 251 deletions(-)
delete mode 100644 examples/2d-arrays1.java
delete mode 100644 examples/arrays.java
delete mode 100644 examples/side-effects.java
delete mode 100644 examples/try-catch-finally.java
diff --git a/examples/2d-arrays1.java b/examples/2d-arrays1.java
deleted file mode 100644
index 6d1d2ba..0000000
--- a/examples/2d-arrays1.java
+++ /dev/null
@@ -1,87 +0,0 @@
-// 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/examples/arrays.java b/examples/arrays.java
deleted file mode 100644
index 18ad95c..0000000
--- a/examples/arrays.java
+++ /dev/null
@@ -1,19 +0,0 @@
-public class Arrays
-{
- public static void main(String[] args)
- {
- int x;
- int y = 4+8;
- int[] a = new int[12];
- int[] b = new int[0];
- a[5] = 2;
- try
- {
- x = b[y];
- }
- catch (ArrayIndexOutOfBoundsException y)
- {
- x = a[5];
- }
- }
-}
\ No newline at end of file
diff --git a/examples/arrays1.java b/examples/arrays1.java
index 4fdd4d0..7dd1376 100644
--- a/examples/arrays1.java
+++ b/examples/arrays1.java
@@ -3,7 +3,7 @@
//https://www.cs.utexas.edu/~scottm/cs307/javacode/codeSamples/ArrayExamples.java
-public class arrays1
+public class Arrays1
{ public static void main(String[] args)
{ int[] list = new int[7];
diff --git a/examples/arrays2.java b/examples/arrays2.java
index bb9bf88..74c8b79 100644
--- a/examples/arrays2.java
+++ b/examples/arrays2.java
@@ -1,8 +1,8 @@
//https://www.tutorialspoint.com/java/java_arrays.htm
-public class TestArray {
+public class Arrays2 {
- public static void main(String[] args) {
+ public static void foo() {
double[] myList = new double[4];
myList[0] = 1.9;
myList[1] = 2.9;
diff --git a/examples/arrays3.java b/examples/arrays3.java
index 212a200..8b30fce 100644
--- a/examples/arrays3.java
+++ b/examples/arrays3.java
@@ -1,10 +1,10 @@
//https://examples.javacodegeeks.com/java-basics/arrays-java-basics/java-string-array-example/
-package com.javacodegeeks.javabasics.stringarray;
+// package com.javacodegeeks.javabasics.stringarray;
-public class JavaStringArrayExample {
+public class Arrays3 {
- public static void main(String args[]) {
+ public static void foo() {
// declare a string array with initial size
String[] schoolbag = new String[4];
diff --git a/examples/loops.java b/examples/loops.java
index 9134308..b22e2e2 100644
--- a/examples/loops.java
+++ b/examples/loops.java
@@ -1,11 +1,9 @@
-
-
-public class C1
+public class Loops
{
- public static void main(String[] args)
- {
-
- for(int i = 0; i < 6; i++)
+ public static void foo()
+ {
+ int i ;
+ for(i = 0; i < 6; i++)
{
for(int j = 0; j < 6; j++)
{
@@ -13,8 +11,6 @@ public class C1
assert j == 1;
}
}
-
-
int x = i;
}
}
\ No newline at end of file
diff --git a/examples/methods.java b/examples/methods.java
index 661059a..c6e58c2 100644
--- a/examples/methods.java
+++ b/examples/methods.java
@@ -1,49 +1,37 @@
-public static class Main
+public class Methods
{
- static int x, y;
- public static void main(String[] args)
- {
- C c1, c2;
- c1 = new C(1);
- c2 = new C(0);
- c1.method1(1, true);
- c2.method1(1, true);
- x = c1.c + c2.c;
- // C.staticMethod();
- }
-
-
-
- public static int method()
- {
- return 1;
- }
-}
+ int c ;
-public class C
-{
- int c;
-
- public C(int init)
- {
- this.c = init;
- }
-
- public static void staticMethod()
- {
- x = 4;
- }
-
- public void method1(int n, boolean b)
- {
+ public Methods(int init) { this.c = init; }
+
+ public int method1() { return 1; }
+
+ public void method2(int n, boolean b) {
assert b;
this.c += n;
if(this.c < 2)
this.method1();
}
- public int method2()
+
+ static int x, y;
+
+ public static int staticmethod1() { return 1; }
+
+ public static void staticmethod2() { x = 4 ; }
+
+ public static void main(String[] args)
{
- return 1;
+ Methods c1, c2;
+ c1 = new Methods(1);
+ c2 = new Methods(0);
+ c1.method2(1, true);
+ c2.method2(1, true);
+ x = c1.c + c2.c;
+ // staticmethod2();
}
-}
\ No newline at end of file
+
+
+
+
+}
diff --git a/examples/objects.java b/examples/objects.java
index 574c846..9aba12a 100644
--- a/examples/objects.java
+++ b/examples/objects.java
@@ -1,45 +1,38 @@
-public class HelloWorld
+public class Objects
{
static int c;
- static Chain chain1, chain2;
+ static CircleChain chain1, chain2;
- public static void main(String[] args)
+ public static void foo()
{
float x = 1;
Circle circle1, circle2;
circle1 = new Circle(0, 0);
circle2 = new Circle(0, 0);
- chain1 = new Chain();
+ chain1 = new CircleChain();
+ chain2 = new CircleChain();
chain1.tail = chain2;
chain1.circle = circle1;
chain2.circle = circle2;
- circle2.center = 2;
-
+ circle2.center = 2;
x = chain1.tail.circle.center;
}
- private static void someFunction()
- {
- c = c + 1;
- }
}
-// The circle class
-public class Circle
-{
+class Circle {
public float center, radius;
-
- public Circle(float center, float radius)
- {
+ public Circle(float center, float radius) {
this.center = center;
this.radius = radius;
}
}
-// A chain of circles
-public class Chain
+class CircleChain
{
public Circle circle;
- public Chain tail;
+ public CircleChain tail;
}
+
+
diff --git a/examples/side-effects.java b/examples/side-effects.java
deleted file mode 100644
index 5626bc6..0000000
--- a/examples/side-effects.java
+++ /dev/null
@@ -1,27 +0,0 @@
-import blabla;
-
-public static class Main
-{
- static int x, y;
- public static void main(String[] args)
- {
- x = 0;
- y = 3;
- int i = 0;
- while(f() < y)
- {
- x = f();
- }
-
- x++;
- x++;
- }
-
-
-
- public static Int f()
- {
- y++;
- return 3;
- }
-}
\ No newline at end of file
diff --git a/examples/simple.java b/examples/simple.java
index 75c864c..a6f4629 100644
--- a/examples/simple.java
+++ b/examples/simple.java
@@ -1,5 +1,5 @@
-public class simple
-{
+public class Simple {
+
// try for example with postcond: returnValue >= 0
int f1(int x) { x++ ; return x ; }
@@ -14,7 +14,7 @@ public class simple
int a ;
// try pcond: returnValue.a >= 0
- simple g1(int delta) { this.a = this.a + delta ; return this ; }
+ Simple g1(int delta) { this.a = this.a + delta ; return this ; }
// try pcond: returnValue >= 0
int g2(int delta) { this.a = this.a + delta ; return this.a ; }
diff --git a/examples/switch.java b/examples/switch.java
index 87b08d7..c82775a 100644
--- a/examples/switch.java
+++ b/examples/switch.java
@@ -1,5 +1,6 @@
-public class Class {
- public static void main(String[] args)
+public class Switch {
+
+ public static void foo()
{
int x, y;
diff --git a/examples/try-catch-finally.java b/examples/try-catch-finally.java
deleted file mode 100644
index 554e394..0000000
--- a/examples/try-catch-finally.java
+++ /dev/null
@@ -1,38 +0,0 @@
-// Source: http://stackoverflow.com/questions/3779285/exception-thrown-in-catch-and-finally-clause
-
-
-class MyExc1 extends Exception {}
-class MyExc2 extends Exception {}
-class MyExc3 extends MyExc2 {}
-
-public class C1 {
- public static void main(String[] args) throws Exception {
- try {
- int x = 1;
-
- try
- {
- throw new MyExc1();
- }
- catch (Exception y)
- {
- }
- finally
- {
- x = 3;
- throw new Exception();
- }
- }
- catch (Exception i)
- {
- throw new MyExc2();
- }
- finally {
- x = 2;
- }
- }
-
- static void q() throws Exception {
-
- }
-}
\ No newline at end of file
diff --git a/src/Javawlp/Engine/WLP.hs b/src/Javawlp/Engine/WLP.hs
index d09dab0..1a1de5c 100644
--- a/src/Javawlp/Engine/WLP.hs
+++ b/src/Javawlp/Engine/WLP.hs
@@ -100,9 +100,16 @@ wlpStmtAlgebra = (fStmtBlock, fIfThen, fIfThenElse, fWhile, fBasicFor, fEnhanced
-- Unrolls a while-loop a finite amount of times
unrollLoop :: Inh -> Int -> Exp -> (Exp -> Exp) -> (Inh -> Exp -> Exp) -> Exp -> Exp
unrollLoop inh 0 g gTrans _ = let var = getVar
- in gTrans . substVar' inh var g . (neg (ExpName (Name [var])) `imp`) . acc inh
+ -- in gTrans . substVar' inh var g . (neg (ExpName (Name [var])) `imp`) . acc inh
+ in gTrans . substVar' inh var g . (neg (ExpName (Name [var])) &*) . acc inh
unrollLoop inh n g gTrans bodyTrans = let var = getVar
- in gTrans . substVar' inh var g . (\q -> (neg (ExpName (Name [var])) `imp` acc inh q) &* ((ExpName (Name [var])) `imp` bodyTrans inh {acc = (unrollLoop inh (n-1) g gTrans bodyTrans)} q))
+ -- in gTrans . substVar' inh var g . (\q -> (neg (ExpName (Name [var])) `imp` acc inh q) &* ((ExpName (Name [var])) `imp` bodyTrans inh {acc = (unrollLoop inh (n-1) g gTrans bodyTrans)} q))
+ -- reformulating it as a disjunction rather than conjunction ; this should be equivalent
+ in gTrans
+ . substVar' inh var g
+ . (\q -> (neg (ExpName (Name [var])) &* acc inh q)
+ |*
+ ((ExpName (Name [var])) &* bodyTrans inh {acc = (unrollLoop inh (n-1) g gTrans bodyTrans)} q))
-- An optimized version of unroll loop to reduce the size of the wlp
unrollLoopOpt :: Inh -> Int -> Exp -> (Exp -> Exp) -> (Inh -> Exp -> Exp) -> Exp -> Exp
--
GitLab