Anzeige
Erschienen in:
2016 | OriginalPaper | Buchkapitel
From Specification to Proof Obligations
verfasst von : Daniel Grahl, Mattias Ulbrich
Erschienen in: Deductive Software Verification – The KeY Book
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Specification with the Java Modeling Language (JML) has been introduced by example in the previous chapter without giving formal definitions of the meaning of JML specifications. Unfortunately, the JML reference manual [Leavens et al., 2013] does not provide a formal semantics, but informal descriptions, often stated in operational terms of the Java language. This is a serious shortcoming since the primary use case of JML is formal specification. Some formal representations from within the JML community have been suggested before [Jacobs and Poll, 2001, Engel, 2005, Darvas and Müller, 2007, Bruns, 2009], but none of them prevailed. Furthermore, over the years several extensions or dialects to JML have emerged (e.g., the extension with dynamic frames by Weiß [2011] that is used in KeY).