We instantiate our framework for a task in specification inference: conditions for commutativity of method. Below, we list our comprehensive results.

Note: preconditions automatically simplified using Z3.

Data Structures

Stack

Methods: peek, pop, push, size

* In this case, false is an ideal TBT precondition but it is only truly safe and not truly maximal.

This is the case when for every positive counterexample produced by our testing based teacher there is a negative counterexample that is L-indistinguishable. In this particular case, our TBT cannot distinguish between any point. That is, all counterexamples become negative. Given an observer method, AllElementsAreEqual() that returns true when all element in stack are equal and false otherwise, our TBT would be able to distinguish the counterexamples.

Queue

Methods: peek, dequeue, enqueue, size

* Same reasoning as in the case for a Stack.

Set

Methods: contains, remove, add, size

Map

Methods: get, set, remove, add

* Same reasoning as in the case for a Stack.

ArrayList

Methods: get, set, add, insert, remove, removeAt, indexOf, lastIndexOf, size

** Cannot confirm if precondition is truly safe or maximal

* Our tool outputs false due to conflict in features.

UndirectedGraph

Methods: addVertex, removeVertex, clearAdjacentEdges, containsEdge, adjacentEdge, isVerticesEmpty, vertexCount, containsVertex, addEdge, removeEdge, isEdgesEmpty, edgeCount, adjacentEdges, adjacentDegree, isAdjacentEdgesEmpty

BinaryHeap

Methods: capacity, count, add, minimum, removeMinimum, removeAt, indexOf, update

** Cannot confirm if precondition is truly safe or maximal

* Too long to express

LidgrenNetworkNetOutgoingMessage

* Too long to express

LidgrenNetworkNetBigInteger

DSA

Hola

CodeContract