Specification and verification of object-oriented programs using supertype abstraction

DOI10.1007/BF01178658zbMath0831.68009MaRDI QIDQ1902305

William E. Weihl, Gary T. Leavens

Publication date: 25 February 1996

Published in: Acta Informatica (Search for Journal in Brave)

zbMATH Keywords

object-oriented programsformal specification language

Mathematics Subject Classification ID

Theory of programming languages (68N15)

Related Items (4)

Specification and verification challenges for sequential object-oriented programs ⋮ A Coalgebraic Semantics of Subtyping ⋮ An assertion-based proof system for multithreaded Java ⋮ Slicing techniques for verification re-use

Uses Software

• Smalltalk
• LARCH
• Eiffel

Cites Work

• Behavioural correctness of data representations
• Non-deterministic data types: Models and implementations
• A theory for nondeterminism, parallelism, communication, and concurrency
• Order-sorted algebra solves the constructor-selector, multiple representation, and coercion problems
• Parameterized Programming
• Logical relations and the typed λ-calculus
• Writing Larch interface language specifications
• Soundness and Completeness of an Axiom System for Program Verification
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Specification and verification of object-oriented programs using supertype abstraction