A Formal Definition of JML in Coq

Más información sobre el 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.