Towards practical proofs of class correctness

DOI10.1007/3-540-44880-2_22MaRDI QIDQ4436978zbMATH OpenFDO

Authors Bertrand Meyer

Publication date 4 December 2003

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2651/26510359.htm

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• A framework for proving contract-equipped classes
• Verifying a class: combining testing and proving
• Proving Theorems About JML Classes
• A case study in class library verification: Java's vector class
• scientific article; zbMATH DE number 3903944

Cited in

(9)

• Reasoning about assignments in recursive data structures
• Verifying a class: combining testing and proving
• Proving Theorems About JML Classes
• A framework for proving contract-equipped classes
• Proving the correctness of behavioural implementations
• Symbolic Verification Method for Definite Iterations over Tuples of Altered Data Structures and Its Application to Pointer Programs
• A Theory of Pointers for the UTP
• Formalization of Refinement Calculus for Reactive Systems
• Algebra of Monotonic Boolean Transformers

This page was built for publication: Towards practical proofs of class correctness

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4436978)