2022-07-04
Reasoning About Active Objects: A Sound and Complete Assertional Proof Method
Publication
Publication
We present a novel assertional proof method for reasoning about global invariant properties of active objects in the context of the Abstract Behavioral Specification (ABS) language. The main result of this paper is a formal justification of the proof method which establishes both its soundness and completeness with respect to a formally defined operational trace semantics.
| Additional Metadata | |
|---|---|
| W. Ahrendt (Wolfgang) , B. Beckert (Bernhard) , R. Bubel (Richard) , E.B. Johnsen (Einar Broch) | |
| doi.org/10.1007/978-3-031-08166-8_9 | |
| Lecture Notes in Computer Science/Lecture Notes in Artificial Intelligence | |
| Organisation | Centrum Wiskunde & Informatica, Amsterdam (CWI), The Netherlands |
|
de Boer, F., & de Gouw, S. (2022). Reasoning About Active Objects: A Sound and Complete Assertional Proof Method. In W. Ahrendt, B. Beckert, R. Bubel, & E. B. Johnsen (Eds.), The Logic of Software. A Tasting Menu of Formal Methods. doi:10.1007/978-3-031-08166-8_9 |
|