Le livre est actuellement en rupture de stock
En savoir plus sur le livre
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.
Achat du livre
A Formal Definition of JML in Coq, Hermann Lehner
- Langue
- Année de publication
- 2012
- product-detail.submit-box.info.binding
- (souple)
Nous vous informerons par e-mail dès que nous l’aurons retrouvé.
Modes de paiement
Personne n'a encore évalué .