We present a completeness proof of the inductive assertion method for object-oriented programs extended with auxiliary variables. The class of programs considered are assumed to compute over structures which include the standard interpretation of Presburger arithmetic. Further, the assertion language is first-order, i.e., quantification only ranges over basic types …
read moreOther presentations
Abstract Object Creation in First Order Dynamic Logic: State of the Art in Key
We present the state of the art in the KeY Java theorem prover, which is based on a first-order object-oriented dynamic logic.This assertion language allows both specifying and verifying properties of objects at the abstraction level of the programming language, abstracting from aspecific implementation of object creation. Objects which …
read moreSpecifying Interfaces in Java in terms of Communication Histories using Attribute Grammars - part 2
We propose a new formal modeling language for the specification of interfaces in Java in terms of communication histories, i.e., sequences of messages. We show how attribute grammars provide a powerful separation of concerns between high-level protocol-oriented properties, which focus on the kind of messages sent and received, and …
read moreSpecifying Interfaces in Java in terms of Communication Histories using Attribute Grammars - part 1
We propose a new formal modeling language for the specification of interfaces in Java in terms of communication histories, i.e., sequences of messages. We show how attribute grammars provide a powerful separation of concerns between high-level protocol-oriented properties, which focus on the kind of messages sent and received, and …
read moreMist: The Programming Language
In this meeting we would like to discuss the development of the Mist programming language. Our goal is to create a new programming language with many promising features, prominently among them an integrated proof framework. The hope is to automatically generate formal proof of correctness, rather than relying solely on …
read more
Page 1 / 1