A Formal Definition of JML in Coq

and its Application to Runtime Assertion Checking

Autori

• Hermann Lehner

Parametri

• 236 pagine
• 9 ore di lettura

• Computer, IT, programmazione

Maggiori informazioni sul libro

The book delves into the formalization of the Java Modeling Language (JML) using the Coq theorem prover, aiming to clarify ambiguous interpretations of JML constructs. It introduces a groundbreaking algorithm for checking assignable clauses at runtime, particularly in the context of dynamic data groups, enhancing data abstraction. The algorithm is efficient with large data structures and has been formally proven to align with JML semantics, demonstrating both its correctness and the practical benefits of the JML formalization for runtime assertion checking.

Lingua: Inglese

Pubblicato: 2012

(In brossura)