From 5f471209d174d23456a23d674a07e45703711d65 Mon Sep 17 00:00:00 2001
From: koen <koenwermer@gmail.com>
Date: Tue, 24 Jan 2017 22:10:35 +0100
Subject: [PATCH] added special syntax to reason about the return value of
methods in the post condition, added some equivalent mutants (c# code),
changed while loops to generate smaller wlp formulas if the loop does not
affect the post condition
---
Equivalent mutations/BST.cs | 126 ++++++++++++++++
Equivalent mutations/Fibonacci.cs | 33 +++++
Equivalent mutations/Heapsort.cs | 66 +++++++++
Equivalent mutations/Matrix.cs | 35 +++++
Equivalent mutations/Mutants/BST_no_parent.cs | 124 ++++++++++++++++
.../Mutants/Fibonacci_no_extra_prints.cs | 32 ++++
.../Mutants/Stack_bool_is_result.cs | 137 +++++++++++++++++
.../Mutants/Stack_constructor_duplication.cs | 138 +++++++++++++++++
.../Mutants/Stack_useless_property.cs | 134 +++++++++++++++++
Equivalent mutations/Stack.cs | 140 ++++++++++++++++++
Main.hs | 100 ++++++++++---
Settings.hs | 15 +-
Verifier.hs | 7 +-
WLP.hs | 12 +-
14 files changed, 1068 insertions(+), 31 deletions(-)
create mode 100644 Equivalent mutations/BST.cs
create mode 100644 Equivalent mutations/Fibonacci.cs
create mode 100644 Equivalent mutations/Heapsort.cs
create mode 100644 Equivalent mutations/Matrix.cs
create mode 100644 Equivalent mutations/Mutants/BST_no_parent.cs
create mode 100644 Equivalent mutations/Mutants/Fibonacci_no_extra_prints.cs
create mode 100644 Equivalent mutations/Mutants/Stack_bool_is_result.cs
create mode 100644 Equivalent mutations/Mutants/Stack_constructor_duplication.cs
create mode 100644 Equivalent mutations/Mutants/Stack_useless_property.cs
create mode 100644 Equivalent mutations/Stack.cs
diff --git a/Equivalent mutations/BST.cs b/Equivalent mutations/BST.cs
new file mode 100644
index 0000000..196e67e
--- /dev/null
+++ b/Equivalent mutations/BST.cs
@@ -0,0 +1,126 @@
+// http://www.sanfoundry.com/csharp-program-binary-search-tree-linked-list/
+
+/*
+ * C# Program to Implement Binary Search Tree using Linked List
+ */
+using System;
+using System.Collections.Generic;
+using System.Text;
+namespace TreeSort
+{
+ class Node
+ {
+ public int item;
+ public Node leftc;
+ public Node rightc;
+ public void display()
+ {
+ Console.Write("[");
+ Console.Write(item);
+ Console.Write("]");
+ }
+ }
+ class Tree
+ {
+ public Node root;
+ public Tree()
+ {
+ root = null;
+ }
+ public Node ReturnRoot()
+ {
+ return root;
+ }
+ public void Insert(int id)
+ {
+ Node newNode = new Node();
+ newNode.item = id;
+ if (root == null)
+ root = newNode;
+ else
+ {
+ Node current = root;
+ Node parent;
+ while (true)
+ {
+ parent = current;
+ if (id < current.item)
+ {
+ current = current.leftc;
+ if (current == null)
+ {
+ parent.leftc = newNode;
+ return;
+ }
+ }
+ else
+ {
+ current = current.rightc;
+ if (current == null)
+ {
+ parent.rightc = newNode;
+ return;
+ }
+ }
+ }
+ }
+ }
+ public void Preorder(Node Root)
+ {
+ if (Root != null)
+ {
+ Console.Write(Root.item + " ");
+ Preorder(Root.leftc);
+ Preorder(Root.rightc);
+ }
+ }
+ public void Inorder(Node Root)
+ {
+ if (Root != null)
+ {
+ Inorder(Root.leftc);
+ Console.Write(Root.item + " ");
+ Inorder(Root.rightc);
+ }
+ }
+ public void Postorder(Node Root)
+ {
+ if (Root != null)
+ {
+ Postorder(Root.leftc);
+ Postorder(Root.rightc);
+ Console.Write(Root.item + " ");
+ }
+ }
+ }
+ class Program
+ {
+ static void Main(string[] args)
+ {
+ Tree theTree = new Tree();
+ theTree.Insert(20);
+ theTree.Insert(25);
+ theTree.Insert(45);
+ theTree.Insert(15);
+ theTree.Insert(67);
+ theTree.Insert(43);
+ theTree.Insert(80);
+ theTree.Insert(33);
+ theTree.Insert(67);
+ theTree.Insert(99);
+ theTree.Insert(91);
+ Console.WriteLine("Inorder Traversal : ");
+ theTree.Inorder(theTree.ReturnRoot());
+ Console.WriteLine(" ");
+ Console.WriteLine();
+ Console.WriteLine("Preorder Traversal : ");
+ theTree.Preorder(theTree.ReturnRoot());
+ Console.WriteLine(" ");
+ Console.WriteLine();
+ Console.WriteLine("Postorder Traversal : ");
+ theTree.Postorder(theTree.ReturnRoot());
+ Console.WriteLine(" ");
+ Console.ReadLine();
+ }
+ }
+}
\ No newline at end of file
diff --git a/Equivalent mutations/Fibonacci.cs b/Equivalent mutations/Fibonacci.cs
new file mode 100644
index 0000000..b235082
--- /dev/null
+++ b/Equivalent mutations/Fibonacci.cs
@@ -0,0 +1,33 @@
+// http://www.sanfoundry.com/csharp-program-generate-fibonocci-series/
+
+/*
+ * C# Program to Generate Fibonacci Series
+ */
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+
+namespace fibonaci
+{
+ class Program
+ {
+ static void Main(string[] args)
+ {
+ int i, count, f1 = 0, f2 = 1, f3 = 0;
+ Console.Write("Enter the Limit : ");
+ count = int.Parse(Console.ReadLine());
+ Console.WriteLine(f1);
+ Console.WriteLine(f2);
+ for (i = 0; i <= count; i++)
+ {
+ f3 = f1 + f2;
+ Console.WriteLine(f3);
+ f1 = f2;
+ f2 = f3;
+ }
+ Console.ReadLine();
+
+ }
+ }
+}
\ No newline at end of file
diff --git a/Equivalent mutations/Heapsort.cs b/Equivalent mutations/Heapsort.cs
new file mode 100644
index 0000000..788b297
--- /dev/null
+++ b/Equivalent mutations/Heapsort.cs
@@ -0,0 +1,66 @@
+// http://www.sanfoundry.com/csharp-program-heap-sort/
+
+/*
+ * C# Program to Demonstrate Heap Sort
+ */
+using System;
+class heap
+{
+ int[] r = { 2,5,1,10,6,9,3,7,4,8};
+ public void hsort()
+ {
+ int i, t;
+ for (i = 5; i >= 0; i--)
+ {
+ adjust(i, 9);
+ }
+ for (i = 8; i >= 0; i--)
+ {
+ t = r[i + 1];
+ r[i + 1] = r[0];
+ r[0] = t;
+ adjust(0, i);
+ }
+ }
+ private void adjust(int i, int n)
+ {
+ int t, j;
+ try
+ {
+ t = r[i];
+ j = 2 * i;
+ while (j <= n)
+ {
+ if (j < n && r[j] < r[j + 1])
+ j++;
+ if (t >=r[j])
+ break;
+ r[j / 2] = r[j];
+ j *= 2;
+ }
+ r[j / 2] = t;
+ }
+ catch (IndexOutOfRangeException e)
+ {
+ Console.WriteLine("Array Out of Bounds ", e);
+ }
+ }
+ public void print()
+ {
+ for (int i = 0; i < 10; i++)
+ {
+ Console.WriteLine("{0}", r[i]);
+ }
+
+ }
+ public static void Main()
+ {
+ heap obj = new heap();
+ Console.WriteLine("Elements Before sorting : ");
+ obj.print();
+ obj.hsort();
+ Console.WriteLine("Elements After sorting : ");
+ obj.print();
+ Console.Read();
+ }
+}
\ No newline at end of file
diff --git a/Equivalent mutations/Matrix.cs b/Equivalent mutations/Matrix.cs
new file mode 100644
index 0000000..28e553e
--- /dev/null
+++ b/Equivalent mutations/Matrix.cs
@@ -0,0 +1,35 @@
+// http://www.java2s.com/Code/CSharp/2D-Graphics/MultiplytwoMatrixes.htm
+
+using System;
+using System.Collections.Generic;
+using System.Text;
+
+
+public class Matrix
+{
+ public static double[,] Mul(double[,] a, double[,] b)
+ {
+ if (a.GetLength(1) != b.GetLength(0))
+ throw new ArgumentException();
+ double[,] reuslt = new double[a.GetLength(0), b.GetLength(1)];
+ for (int i = 0; i < a.GetLength(0); i++)
+ for (int j = 0; j < b.GetLength(1); j++)
+ {
+ for (int k = 0; k < a.GetLength(1); k++)
+ {
+ reuslt[i, j] += a[i, k] * b[k, j];
+ }
+ }
+ return reuslt;
+ }
+ public static double[,] MulDiag(double[,] a, double[] b)
+ {
+ if (a.GetLength(1) != b.GetLength(0))
+ throw new ArgumentException();
+ double[,] reuslt = new double[a.GetLength(0), b.GetLength(0)];
+ for (int i = 0; i < a.GetLength(0); i++)
+ for (int j = 0; j < b.GetLength(0); j++)
+ reuslt[i, j] = a[i, j] * b[j];
+ return reuslt;
+ }
+}
\ No newline at end of file
diff --git a/Equivalent mutations/Mutants/BST_no_parent.cs b/Equivalent mutations/Mutants/BST_no_parent.cs
new file mode 100644
index 0000000..c1ab587
--- /dev/null
+++ b/Equivalent mutations/Mutants/BST_no_parent.cs
@@ -0,0 +1,124 @@
+// http://www.sanfoundry.com/csharp-program-binary-search-tree-linked-list/
+
+/*
+ * C# Program to Implement Binary Search Tree using Linked List
+ */
+using System;
+using System.Collections.Generic;
+using System.Text;
+namespace TreeSort
+{
+ class Node
+ {
+ public int item;
+ public Node leftc;
+ public Node rightc;
+ public void display()
+ {
+ Console.Write("[");
+ Console.Write(item);
+ Console.Write("]");
+ }
+ }
+ class Tree
+ {
+ public Node root;
+ public Tree()
+ {
+ root = null;
+ }
+ public Node ReturnRoot()
+ {
+ return root;
+ }
+ public void Insert(int id)
+ {
+ Node newNode = new Node();
+ newNode.item = id;
+ if (root == null)
+ root = newNode;
+ else
+ {
+ Node current = root;
+ while (true)
+ {
+ if (id < current.item)
+ {
+ if (current.leftc == null)
+ {
+ current.leftc = newNode;
+ return;
+ }
+ current = current.leftc;
+ }
+ else
+ {
+ if (current.rightc == null)
+ {
+ current.rightc = newNode;
+ return;
+ }
+ current = current.rightc;
+ }
+ }
+ }
+ }
+ public void Preorder(Node Root)
+ {
+ if (Root != null)
+ {
+ Console.Write(Root.item + " ");
+ Preorder(Root.leftc);
+ Preorder(Root.rightc);
+ }
+ }
+ public void Inorder(Node Root)
+ {
+ if (Root != null)
+ {
+ Inorder(Root.leftc);
+ Console.Write(Root.item + " ");
+ Inorder(Root.rightc);
+ }
+ }
+ public void Postorder(Node Root)
+ {
+ if (Root != null)
+ {
+ Postorder(Root.leftc);
+ Postorder(Root.rightc);
+ Console.Write(Root.item + " ");
+ }
+ }
+ }
+ class Program
+ {
+ static void Main(string[] args)
+ {
+ Tree theTree = new Tree();
+ theTree.Insert(20);
+ theTree.Insert(25);
+ theTree.Insert(45);
+ theTree.Insert(15);
+ theTree.Insert(67);
+ theTree.Insert(43);
+ theTree.Insert(80);
+ theTree.Insert(33);
+ theTree.Insert(67);
+ theTree.Insert(99);
+ theTree.Insert(91);
+ Console.WriteLine("Inorder Traversal : ");
+ theTree.Inorder(theTree.ReturnRoot());
+ Console.WriteLine(" ");
+ Console.WriteLine();
+ Console.WriteLine("Preorder Traversal : ");
+ theTree.Preorder(theTree.ReturnRoot());
+ Console.WriteLine(" ");
+ Console.WriteLine();
+ Console.WriteLine("Postorder Traversal : ");
+ theTree.Postorder(theTree.ReturnRoot());
+ Console.WriteLine(" ");
+ Console.ReadLine();
+ }
+ }
+}
\ No newline at end of file
diff --git a/Equivalent mutations/Mutants/Fibonacci_no_extra_prints.cs b/Equivalent mutations/Mutants/Fibonacci_no_extra_prints.cs
new file mode 100644
index 0000000..eb68898
--- /dev/null
+++ b/Equivalent mutations/Mutants/Fibonacci_no_extra_prints.cs
@@ -0,0 +1,32 @@
+// http://www.sanfoundry.com/csharp-program-generate-fibonocci-series/
+
+/*
+ * C# Program to Generate Fibonacci Series
+ */
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+
+namespace fibonaci
+{
+ class Program
+ {
+ static void Main(string[] args)
+ {
+ int i, count, f1 = 0, f2 = 1, f3 = 0;
+ Console.Write("Enter the Limit : ");
+ count = int.Parse(Console.ReadLine());
+
+ for (i = 0; i <= count + 2; i++)
+ {
+ f3 = f1 + f2;
+ Console.WriteLine(f1);
+ f1 = f2;
+ f2 = f3;
+ }
+ Console.ReadLine();
+
+ }
+ }
+}
\ No newline at end of file
diff --git a/Equivalent mutations/Mutants/Stack_bool_is_result.cs b/Equivalent mutations/Mutants/Stack_bool_is_result.cs
new file mode 100644
index 0000000..13ef6b4
--- /dev/null
+++ b/Equivalent mutations/Mutants/Stack_bool_is_result.cs
@@ -0,0 +1,137 @@
+// http://www.sanfoundry.com/csharp-program-stack-push-pop/
+
+/*
+ * C# Program to Implement Stack with Push and Pop operations
+ */
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Threading.Tasks;
+namespace ConsoleApplication1
+{
+ class Program
+ {
+ static void Main(string[] args)
+ {
+ stack st = new stack();
+ while (true)
+ {
+ Console.Clear();
+ Console.WriteLine("\nStack MENU(size -- 10)");
+ Console.WriteLine("1. Add an element");
+ Console.WriteLine("2. See the Top element.");
+ Console.WriteLine("3. Remove top element.");
+ Console.WriteLine("4. Display stack elements.");
+ Console.WriteLine("5. Exit");
+ Console.Write("Select your choice: ");
+ int choice = Convert.ToInt32(Console.ReadLine());
+ switch (choice)
+ {
+ case 1:
+ Console.WriteLine("Enter an Element : ");
+ st.Push(Console.ReadLine());
+ break;
+
+ case 2: Console.WriteLine("Top element is: {0}", st.Peek());
+ break;
+
+ case 3: Console.WriteLine("Element removed: {0}", st.Pop());
+ break;
+
+ case 4: st.Display();
+ break;
+
+ case 5: System.Environment.Exit(1);
+ break;
+ }
+ Console.ReadKey();
+ }
+ }
+ }
+
+ interface StackADT
+ {
+ Boolean isEmpty();
+ void Push(Object element);
+ Object Pop();
+ Object Peek();
+ void Display();
+ }
+ class stack : StackADT
+ {
+ private int StackSize;
+ public int StackSizeSet
+ {
+ get { return StackSize; }
+ set { StackSize = value; }
+ }
+ public int top;
+ Object[] item;
+ public stack()
+ {
+ StackSizeSet = 10;
+ item = new Object[StackSizeSet];
+ top = -1;
+ }
+ public stack(int capacity)
+ {
+ StackSizeSet = capacity;
+ item = new Object[StackSizeSet];
+ top = -1;
+ }
+ public bool isEmpty()
+ {
+ return top == -1;
+ }
+ public void Push(object element)
+ {
+ if (top == (StackSize - 1))
+ {
+ Console.WriteLine("Stack is full!");
+ }
+
+ else
+ {
+
+ item[++top] = element;
+ Console.WriteLine("Item pushed successfully!");
+ }
+ }
+ public object Pop()
+ {
+ if (isEmpty())
+ {
+ Console.WriteLine("Stack is empty!");
+ return "No elements";
+ }
+ else
+ {
+
+ return item[top--];
+ }
+ }
+ public object Peek()
+ {
+ if (isEmpty())
+ {
+
+ Console.WriteLine("Stack is empty!");
+ return "No elements";
+ }
+ else
+ {
+ return item[top];
+ }
+ }
+
+
+ public void Display()
+ {
+ for (int i = top; i > -1; i--)
+ {
+
+ Console.WriteLine("Item {0}: {1}", (i + 1), item[i]);
+ }
+ }
+ }
diff --git a/Equivalent mutations/Mutants/Stack_constructor_duplication.cs b/Equivalent mutations/Mutants/Stack_constructor_duplication.cs
new file mode 100644
index 0000000..6c390e8
--- /dev/null
+++ b/Equivalent mutations/Mutants/Stack_constructor_duplication.cs
@@ -0,0 +1,138 @@
+// http://www.sanfoundry.com/csharp-program-stack-push-pop/
+
+/*
+ * C# Program to Implement Stack with Push and Pop operations
+ */
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Threading.Tasks;
+namespace ConsoleApplication1
+{
+ class Program
+ {
+ static void Main(string[] args)
+ {
+ stack st = new stack();
+ while (true)
+ {
+ Console.Clear();
+ Console.WriteLine("\nStack MENU(size -- 10)");
+ Console.WriteLine("1. Add an element");
+ Console.WriteLine("2. See the Top element.");
+ Console.WriteLine("3. Remove top element.");
+ Console.WriteLine("4. Display stack elements.");
+ Console.WriteLine("5. Exit");
+ Console.Write("Select your choice: ");
+ int choice = Convert.ToInt32(Console.ReadLine());
+ switch (choice)
+ {
+ case 1:
+ Console.WriteLine("Enter an Element : ");
+ st.Push(Console.ReadLine());
+ break;
+
+ case 2: Console.WriteLine("Top element is: {0}", st.Peek());
+ break;
+
+ case 3: Console.WriteLine("Element removed: {0}", st.Pop());
+ break;
+
+ case 4: st.Display();
+ break;
+
+ case 5: System.Environment.Exit(1);
+ break;
+ }
+ Console.ReadKey();
+ }
+ }
+ }
+
+ interface StackADT
+ {
+ Boolean isEmpty();
+ void Push(Object element);
+ Object Pop();
+ Object Peek();
+ void Display();
+ }
+ class stack : StackADT
+ {
+ private int StackSize;
+ public int StackSizeSet
+ {
+ get { return StackSize; }
+ set { StackSize = value; }
+ }
+ public int top;
+ Object[] item;
+ public stack()
+ : stack(10)
+ {
+ }
+ public stack(int capacity)
+ {
+ StackSizeSet = capacity;
+ item = new Object[StackSizeSet];
+ top = -1;
+ }
+ public bool isEmpty()
+ {
+ if (top == -1) return true;
+
+ return false;
+ }
+ public void Push(object element)
+ {
+ if (top == (StackSize - 1))
+ {
+ Console.WriteLine("Stack is full!");
+ }
+
+ else
+ {
+
+ item[++top] = element;
+ Console.WriteLine("Item pushed successfully!");
+ }
+ }
+ public object Pop()
+ {
+ if (isEmpty())
+ {
+ Console.WriteLine("Stack is empty!");
+ return "No elements";
+ }
+ else
+ {
+
+ return item[top--];
+ }
+ }
+ public object Peek()
+ {
+ if (isEmpty())
+ {
+
+ Console.WriteLine("Stack is empty!");
+ return "No elements";
+ }
+ else
+ {
+ return item[top];
+ }
+ }
+
+
+ public void Display()
+ {
+ for (int i = top; i > -1; i--)
+ {
+
+ Console.WriteLine("Item {0}: {1}", (i + 1), item[i]);
+ }
+ }
+ }
+}
\ No newline at end of file
diff --git a/Equivalent mutations/Mutants/Stack_useless_property.cs b/Equivalent mutations/Mutants/Stack_useless_property.cs
new file mode 100644
index 0000000..aa75d32
--- /dev/null
+++ b/Equivalent mutations/Mutants/Stack_useless_property.cs
@@ -0,0 +1,134 @@
+// http://www.sanfoundry.com/csharp-program-stack-push-pop/
+
+/*
+ * C# Program to Implement Stack with Push and Pop operations
+ */
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Threading.Tasks;
+namespace ConsoleApplication1
+{
+ class Program
+ {
+ static void Main(string[] args)
+ {
+ stack st = new stack();
+ while (true)
+ {
+ Console.Clear();
+ Console.WriteLine("\nStack MENU(size -- 10)");
+ Console.WriteLine("1. Add an element");
+ Console.WriteLine("2. See the Top element.");
+ Console.WriteLine("3. Remove top element.");
+ Console.WriteLine("4. Display stack elements.");
+ Console.WriteLine("5. Exit");
+ Console.Write("Select your choice: ");
+ int choice = Convert.ToInt32(Console.ReadLine());
+ switch (choice)
+ {
+ case 1:
+ Console.WriteLine("Enter an Element : ");
+ st.Push(Console.ReadLine());
+ break;
+
+ case 2: Console.WriteLine("Top element is: {0}", st.Peek());
+ break;
+
+ case 3: Console.WriteLine("Element removed: {0}", st.Pop());
+ break;
+
+ case 4: st.Display();
+ break;
+
+ case 5: System.Environment.Exit(1);
+ break;
+ }
+ Console.ReadKey();
+ }
+ }
+ }
+
+ interface StackADT
+ {
+ Boolean isEmpty();
+ void Push(Object element);
+ Object Pop();
+ Object Peek();
+ void Display();
+ }
+ class stack : StackADT
+ {
+ private int StackSize;
+
+ public int top;
+ Object[] item;
+ public stack()
+ {
+ item = new Object[10];
+ top = -1;
+ }
+ public stack(int capacity)
+ {
+ item = new Object[capacity];
+ top = -1;
+ }
+ public bool isEmpty()
+ {
+ if (top == -1) return true;
+
+ return false;
+ }
+ public void Push(object element)
+ {
+ if (top == (StackSize - 1))
+ {
+ Console.WriteLine("Stack is full!");
+ }
+
+ else
+ {
+
+ item[++top] = element;
+ Console.WriteLine("Item pushed successfully!");
+ }
+ }
+ public object Pop()
+ {
+ if (isEmpty())
+ {
+ Console.WriteLine("Stack is empty!");
+ return "No elements";
+ }
+ else
+ {
+
+ return item[top--];
+ }
+ }
+ public object Peek()
+ {
+ if (isEmpty())
+ {
+
+ Console.WriteLine("Stack is empty!");
+ return "No elements";
+ }
+ else
+ {
+ return item[top];
+ }
+ }
+
+
+ public void Display()
+ {
+ for (int i = top; i > -1; i--)
+ {
+
+ Console.WriteLine("Item {0}: {1}", (i + 1), item[i]);
+ }
+ }
+ }
+}
\ No newline at end of file
diff --git a/Equivalent mutations/Stack.cs b/Equivalent mutations/Stack.cs
new file mode 100644
index 0000000..65ff81e
--- /dev/null
+++ b/Equivalent mutations/Stack.cs
@@ -0,0 +1,140 @@
+// http://www.sanfoundry.com/csharp-program-stack-push-pop/
+
+/*
+ * C# Program to Implement Stack with Push and Pop operations
+ */
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Text;
+using System.Threading.Tasks;
+namespace ConsoleApplication1
+{
+ class Program
+ {
+ static void Main(string[] args)
+ {
+ stack st = new stack();
+ while (true)
+ {
+ Console.Clear();
+ Console.WriteLine("\nStack MENU(size -- 10)");
+ Console.WriteLine("1. Add an element");
+ Console.WriteLine("2. See the Top element.");
+ Console.WriteLine("3. Remove top element.");
+ Console.WriteLine("4. Display stack elements.");
+ Console.WriteLine("5. Exit");
+ Console.Write("Select your choice: ");
+ int choice = Convert.ToInt32(Console.ReadLine());
+ switch (choice)
+ {
+ case 1:
+ Console.WriteLine("Enter an Element : ");
+ st.Push(Console.ReadLine());
+ break;
+
+ case 2: Console.WriteLine("Top element is: {0}", st.Peek());
+ break;
+
+ case 3: Console.WriteLine("Element removed: {0}", st.Pop());
+ break;
+
+ case 4: st.Display();
+ break;
+
+ case 5: System.Environment.Exit(1);
+ break;
+ }
+ Console.ReadKey();
+ }
+ }
+ }
+
+ interface StackADT
+ {
+ Boolean isEmpty();
+ void Push(Object element);
+ Object Pop();
+ Object Peek();
+ void Display();
+ }
+ class stack : StackADT
+ {
+ private int StackSize;
+ public int StackSizeSet
+ {
+ get { return StackSize; }
+ set { StackSize = value; }
+ }
+ public int top;
+ Object[] item;
+ public stack()
+ {
+ StackSizeSet = 10;
+ item = new Object[StackSizeSet];
+ top = -1;
+ }
+ public stack(int capacity)
+ {
+ StackSizeSet = capacity;
+ item = new Object[StackSizeSet];
+ top = -1;
+ }
+ public bool isEmpty()
+ {
+ if (top == -1) return true;
+
+ return false;
+ }
+ public void Push(object element)
+ {
+ if (top == (StackSize - 1))
+ {
+ Console.WriteLine("Stack is full!");
+ }
+
+ else
+ {
+
+ item[++top] = element;
+ Console.WriteLine("Item pushed successfully!");
+ }
+ }
+ public object Pop()
+ {
+ if (isEmpty())
+ {
+ Console.WriteLine("Stack is empty!");
+ return "No elements";
+ }
+ else
+ {
+
+ return item[top--];
+ }
+ }
+ public object Peek()
+ {
+ if (isEmpty())
+ {
+
+ Console.WriteLine("Stack is empty!");
+ return "No elements";
+ }
+ else
+ {
+ return item[top];
+ }
+ }
+
+
+ public void Display()
+ {
+ for (int i = top; i > -1; i--)
+ {
+
+ Console.WriteLine("Item {0}: {1}", (i + 1), item[i]);
+ }
+ }
+ }
+}
\ No newline at end of file
diff --git a/Main.hs b/Main.hs
index 3e9f6be..efe1568 100644
--- a/Main.hs
+++ b/Main.hs
@@ -22,8 +22,11 @@ mutantsDir = joinPath ["..", testFile ++ " mutants"]
main :: IO ()
main = do
+ -- Parse the original sourceCode
+ (env, decls, methods) <- parseFile sourcePath
+
-- Get the wlp per method of the original source code
- (env, wlpOriginal) <- wlpMethods sourcePath
+ wlpOriginal <- wlpMethods env decls methods
-- Get the names of the folders containing the mutants (MAJOR creates a folder for every mutant)
mutationFolders <- listDirectory mutantsDir
@@ -32,13 +35,17 @@ main = do
let mutationPaths = map (\n -> joinPath [mutantsDir, n, testFile ++ ".java"]) mutationFolders
-- Calculate the wlp per method of all the mutants
- wlpMutants <- mapM (\path -> wlpMethods path >>= return . (path, ) . snd) mutationPaths
+ wlpMutants <- mapM (\path -> parseFile path >>= (\(env', decls', methods') -> wlpMethods env' decls' methods') >>= return . (path, )) mutationPaths
- mapM_ (compareWlps env wlpOriginal) wlpMutants
+ -- A list containing a 1 or 0 per mutant, indicating the number of errors found
+ errorsFound <- mapM (compareWlps env decls wlpOriginal) wlpMutants
--- | Calculates the wlp for every method in the source file. Also returns the type environment
-wlpMethods :: FilePath -> IO (TypeEnv, [(Ident, Exp)])
-wlpMethods s = do
+ putStrLn ("Total number of mutants: " ++ show (length errorsFound))
+ putStrLn ("Number of mutants in which we found an error: " ++ show (sum errorsFound))
+
+-- Parses a files and extracts the necessary information from the compilation unit
+parseFile :: FilePath -> IO (TypeEnv, [TypeDecl], [Ident])
+parseFile s = do
-- Get the source code
source <- readFile s
@@ -50,26 +57,71 @@ wlpMethods s = do
let methods = getMethodIds decls
let env = getTypeEnv compUnit decls methods
- -- Calculate the wlp per method
- r <- mapM (\ident -> wlpMethod compUnit env decls ident >>= return . (ident, )) methods
-
- return (env, r)
+ return (env, decls, methods)
+
+-- | Calculates the wlp for every method in the source file. Also returns the type environment
+wlpMethods :: TypeEnv -> [TypeDecl] -> [Ident] -> IO [(Ident, Exp)]
+wlpMethods env decls methods = mapM (\ident -> wlpMethod env decls ident >>= return . (ident, )) methods' where
+ methods' = if ignoreMainMethod then filter (/= Ident "main") methods else methods
-- | Calculates the wlp for a given method
-wlpMethod :: CompilationUnit -> TypeEnv -> [TypeDecl] -> Ident -> IO Exp
-wlpMethod compUnit env decls ident = do
- let pred = wlpWithEnv decls env (fromJust' "wlpMethod" $ getMethod decls ident) postCond'
+wlpMethod :: TypeEnv -> [TypeDecl] -> Ident -> IO Exp
+wlpMethod env decls ident = do
+ -- Find the return type of the method
+ let returnType = getMethodType decls ident
+
+ -- Add returnValue to the type environment with the correct type
+ let env' = case returnType of
+ Nothing -> env
+ Just t -> (Name [Ident "returnValue"], t) : (Name [Ident "returnValueVar"], t) : env
+
+ -- Calculate the wlp. Note that the post condition might depend on the type of the function
+ let pred = wlpWithEnv decls env' (fromJust' "wlpMethod" $ getMethod decls ident) (getPostCond returnType)
return pred
--- | Compares the wlp per method of a program S and mutation S' by verifying that (wlp (S, m) q => wlp (S', m) q) holds for every method m
-compareWlps :: TypeEnv -> [(Ident, Exp)] -> (String, [(Ident, Exp)]) -> IO ()
-compareWlps env s (path, s') = mapM_ compareMethod s where
- compareMethod (ident, e) = case lookup ident s' of
- Nothing -> putStrLn ("The method \'" ++ show ident ++ "\' is missing in one of the mutations.")
- Just e' -> if unsafeIsTrue env (e `imp` e') then return () else putStrLn ("error detected in mutation: " ++ path)
+-- | Compares the wlp per method of a program S and mutation S' by verifying that (wlp (S, m) q => wlp (S', m) q) holds for every method m. Returns 0 if it holds and 1 if it doesn't hold
+compareWlps :: TypeEnv -> [TypeDecl] -> [(Ident, Exp)] -> (String, [(Ident, Exp)]) -> IO Int
+compareWlps env decls s (path, s') = do
+ -- Get a list with for every method the number of errors found (1 or 0)
+ errorsFound <- mapM compareMethod s
+ -- Return 1 if we found at least 1 error
+ return (if sum errorsFound > 0 then 1 else 0)
+ where
+ compareMethod (ident, e) = case lookup ident s' of
+ Nothing -> putStrLn ("The method \'" ++ show ident ++ "\' is missing in one of the mutations.") >> return 0 -- print a warning and return 0 errors found
+ Just e' -> if unsafeIsTrue (extendEnv env decls ident) (e `imp` e') then return 0 else putStrLn ("error detected in mutation: " ++ path ++ " method: " ++ prettyPrint ident) >> return 1 -- print a message and return 1 error found
+ -- Adds returnValue to the type environment with the correct type
+ extendEnv env decls ident = case getMethodType decls ident of
+ Nothing -> env
+ Just t -> (Name [Ident "returnValue"], t) : (Name [Ident "returnValueVar"], t) : env
--- The post-condition (for testing)
-postCond' :: Exp
-postCond' = case parser Language.Java.Parser.exp postCond of
- Right e -> e
- _ -> error "syntax error in post-condition"
\ No newline at end of file
+-- Gets the right post-condition given the type of a method
+getPostCond :: Maybe Type -> Exp
+getPostCond t = case parser Language.Java.Parser.exp postCond' of
+ Right e -> e
+ _ -> error "syntax error in post-condition"
+ where postCond' = case t of
+ Nothing -> postCondVoid
+ Just (RefType _) -> postCondRefType
+ Just (PrimType _) -> postCondPrimType
+
+-- Calculate the wlp (for testing purposes)
+calcWlp :: IO ()
+calcWlp = do
+ source <- readFile (joinPath ["Tests", testFile ++ ".java"])
+
+ let result = parser compilationUnit source
+
+ case result of
+ Left error -> print error
+ Right compUnit -> do
+ let decls = getDecls compUnit
+ let methods = if ignoreMainMethod then filter (/= Ident "main") (getMethodIds decls) else getMethodIds decls
+ let env = getTypeEnv compUnit decls methods
+ let printMethodWlp = (\ident e -> putStrLn (prettyPrint ident ++ ":\r\n" ++ prettyPrint e ++ "\r\n" ++ (if unsafeIsTrue (extendEnv env decls ident) e then "WLP evaluates to true" else (if unsafeIsFalse (extendEnv env decls ident) e then "WLP evaluates to false" else "undecidable")) ++ "\r\n"))
+ mapM_ (\ident -> wlpMethod env decls ident >>= printMethodWlp ident) methods
+ where
+ -- Adds returnValue to the type environment with the correct type
+ extendEnv env decls ident = case getMethodType decls ident of
+ Nothing -> env
+ Just t -> (Name [Ident "returnValue"], t) : (Name [Ident "returnValueVar"], t) : env
\ No newline at end of file
diff --git a/Settings.hs b/Settings.hs
index 0e4b16f..1a9629b 100644
--- a/Settings.hs
+++ b/Settings.hs
@@ -1,8 +1,19 @@
module Settings where
-testFile, postCond :: String
+testFile, postCondVoid, postCondRefType, postCondPrimType :: String
testFile = "arrays1"
-postCond = "(true)"
+
+-- The post condition may depend on the type of the method we are looking at
+postCondVoid = "true"
+postCondRefType = "returnValue != null"
+postCondPrimType = "returnValue == returnValueVar"
+
+-- When ignoreLibMethods is true, library calls will simply be ignored. When false, we consider library methods but make no assumptions about them (so the WLP will be true)
+-- To prevent insanely long calculation times, we may decide to not calculate the wlp of the main method when ignoring library methods
+ignoreLibMethods, ignoreMainMethod :: Bool
+ignoreLibMethods = False
+ignoreMainMethod = False
+
nrOfUnroll :: Int
nrOfUnroll = 1
\ No newline at end of file
diff --git a/Verifier.hs b/Verifier.hs
index c2406e9..d05c8c5 100644
--- a/Verifier.hs
+++ b/Verifier.hs
@@ -7,6 +7,7 @@ import System.IO.Unsafe
import Folds
import HelperFunctions
+import Settings
-- | Checks wether the negation is unsatisfiable
@@ -78,6 +79,7 @@ expAssertAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQual
symbol <- mkStringSymbol ("*length(" ++ prettyPrint name ++ ", " ++ show n ++ ")")
mkIntVar symbol
Cond g a1 a2 -> foldExp expAssertAlgebra (Cond g (MethodInv (MethodCall (Name [Ident "*length"]) [a1, (Lit (Int n))])) (MethodInv (MethodCall (Name [Ident "*length"]) [a2, (Lit (Int n))]))) env
+ Lit Null -> mkInteger (-1)
_ -> error ("length of non-array: " ++ prettyPrint a)
_ -> error (prettyPrint invocation)
fArrayAccess arrayIndex env = case arrayIndex of
@@ -98,7 +100,10 @@ expAssertAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQual
Just (PrimType BooleanT) -> mkBoolVar symbol
Just (PrimType FloatT) -> mkRealVar symbol
Just (PrimType DoubleT) -> mkRealVar symbol
- _ -> mkIntVar symbol
+ Just (PrimType IntT) -> mkIntVar symbol
+ Just (RefType _) -> mkIntVar symbol
+ -- For now, we assume library methods return ints. Fixing this would require type information of library methods.
+ t -> if ignoreLibMethods then mkStringSymbol "libMethodCall" >>= mkIntVar else error ("Verifier: Type of " ++ prettyPrint name ++ " unknown or not implemented: " ++ show t)
fPostIncrement = undefined
fPostDecrement = undefined
fPreIncrement = undefined
diff --git a/WLP.hs b/WLP.hs
index c9a796f..92ebee6 100644
--- a/WLP.hs
+++ b/WLP.hs
@@ -41,7 +41,7 @@ wlpStmtAlgebra = (fStmtBlock, fIfThen, fIfThenElse, fWhile, fBasicFor, fEnhanced
in trans . substVar' inh var e' . (\q -> (ExpName (Name [var]) &* s1 inh {acc = id} q) |* (neg (ExpName (Name [var])) &* s2 inh {acc = id} q)) . acc inh
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
+ in (\q -> unrollLoopOpt 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)
fEnhancedFor = error "EnhancedFor"
fEmpty inh = (acc inh) -- Empty does nothing, but still passes control to the next statement
@@ -88,6 +88,10 @@ wlpStmtAlgebra = (fStmtBlock, fIfThen, fIfThenElse, fWhile, fBasicFor, fEnhanced
unrollLoop inh n g gTrans bodyTrans = let var = getVar
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)))
+ -- An optimized version of unroll loop to reduce the size of the wlp
+ unrollLoopOpt :: Inh -> Int -> Exp -> (Exp -> Exp) -> (Exp -> Exp) -> Exp -> Exp
+ unrollLoopOpt inh n g gTrans bodyTrans q | gTrans (bodyTrans q) == q = q -- q is not affected by the loop
+ | otherwise = unrollLoop inh n g gTrans bodyTrans q -- default to the standard version of unroll loop
-- Converts initialization code of a for loop to a statement
initToStmt :: Maybe ForInit -> Stmt
@@ -227,10 +231,10 @@ wlpExpAlgebra = (fLit, fClassLit, fThis, fThisClass, fInstanceCreation, fQualIns
-- Gets the body of the method
getBody :: Inh -> MethodInvocation -> Stmt
getBody inh (MethodCall name _) = case getMethod (decls inh) (getMethodId name) of
- Nothing -> ExpStmt $ MethodInv (MethodCall (Name [Ident "*assume"]) [false])
+ Nothing -> if ignoreLibMethods then Empty else ExpStmt $ MethodInv (MethodCall (Name [Ident "*assume"]) [false])
Just s -> s
getBody inh (PrimaryMethodCall _ _ id _) = case getMethod (decls inh) id of
- Nothing -> ExpStmt $ MethodInv (MethodCall (Name [Ident "*assume"]) [false])
+ Nothing -> if ignoreLibMethods then Empty else ExpStmt $ MethodInv (MethodCall (Name [Ident "*assume"]) [false])
Just s -> s
getBody inh _ = undefined
-- Assigns the supplied parameter values to the parameter variables
@@ -297,7 +301,7 @@ wlp decls = wlpWithEnv decls []
-- | wlp with a given type environment
wlpWithEnv :: [TypeDecl] -> TypeEnv -> Stmt -> Exp -> Exp
-wlpWithEnv decls env = wlp' (Inh id id Nothing env decls [] Nothing (Just (ExpName (Name [Ident "#obj"]))))
+wlpWithEnv decls env = wlp' (Inh id id Nothing env decls [] (Just (Ident "returnValue")) (Just (ExpName (Name [Ident "#obj"]))))
-- wlp' lets you specify the inherited attributes
wlp' :: Inh -> Stmt -> Syn
--
GitLab