Our article in the journal Formal Methods in System Design is now openly available on-line: it describes how to integrate and use Algebraic/Abstract Data Types (ADTs) in the KeY theorem prover, useful for reasoning about the correctness of clients of Java interfaces such as java.util.Collection and its Iterator.
(Joint work with: Jinting Bian, Frank de Boer, Stijn de Gouw.)
Our main insight is to keep a history for each instance of an interface, which can then be used in the specification of method contracts (using the design-by-contract methodology). In our approach, histories are modeled by ADTs, both as algebraic data type ánd abstract data type. A history does not predict the future state of an object, but it does allow for the expression of expectations and acceptable behavior. This is important in the verification of real-world software, to make sure no unexpected behavior such as errors and crashes occur.
#software #java #formalverification #theory
Back to top