Higher -order logic can be used for meaning representation in natural language processing to encode the semantic relationships in text. Alternatively, using a formal specification language for meaning representation i...
详细信息
Higher -order logic can be used for meaning representation in natural language processing to encode the semantic relationships in text. Alternatively, using a formal specification language for meaning representation is more precise for specifying programs and widely supported by automatic theorem provers, while deductive verification based on higher order logic is less common for mainstream programming languages. This paper addresses the research question of translating higher -order logic meaning representations generated from method -level code comments into a formal specification language that extends first -order logic. Doing so requires resolving possible ambiguities in determining the appropriate semantics for predicates. This is an open challenge in the path toward using natural language processing with formal methods. To address this, the paper proposes an approach and constructs a compiler for translating meaning representations, generated from java programs with method -level comments, into java modelling language. We evaluate the compiler on a set of representative benchmarks, including programs and specifications from the java API, by generating java modelling language specifications and statically checking them with a theorem prover. Results show that in 94% of the cases java modelling language is accurately generated and in 97% of those cases it can be automatically checked with a state-of-the-art theorem prover.
java code can be annotated with formal specifications using the java modelling language (JML). Previous work has provided IDE plugins intended to help write JML, but mostly for the Eclipse IDE. We introduce IntelliJML...
详细信息
ISBN:
(纸本)9781450385435
java code can be annotated with formal specifications using the java modelling language (JML). Previous work has provided IDE plugins intended to help write JML, but mostly for the Eclipse IDE. We introduce IntelliJML, a JML plugin for IntelliJ IDEA, with a focus on ease of use and maintainability. Features such as syntax, semantic, and type checking, as well as syntax highlighting and code completion are integrated into the plugin. The plugin can also be extended in the future to add more features.
Static checking is key for the security of software components. As a component model, this paper considers a java class enriched with annotations from the java modelling language (JML). It defines a formal execution s...
详细信息
Static checking is key for the security of software components. As a component model, this paper considers a java class enriched with annotations from the java modelling language (JML). It defines a formal execution semantics for repetitive method invocations from this annotated class, called the class in isolation semantics. Afterwards, a pattern of liveness properties is defined, together with its formal semantics, providing a foundation for both static and runtime checking. This pattern is then inscribed in a complete language of temporal properties, called java temporal pattern language, extending JML. The authors particularly address the veri. cation of liveness properties by automatically translating the temporal properties into JML annotations for this class. This automatic translation is implemented in a tool called JML annotation generator. Correctness of the generated annotations ensures that the temporal property is established for the executions of the class in isolation.
暂无评论