Paper Info
Title
Specification and Verification of Object-Oriented Programs Using Supertype Abstraction.
Abstract
We present a formal specification language and a formal verification logic for a simple object-oriented programming language. The language is applicative and statically typed, and supports subtyping and message-passing. The verification logic relies on a behavioral notion of subtyping that captures the intuition that a subtype behaves like its supertypes. We give a formal definition for legal subtype relations, based on the specified behavior of objects, and show that this definition is sufficient to ensure the soundness of the verification logic. The verification logic reflects the way programmers reason informally about object-oriented programs, in that it allows them to use static type information, which avoids the need to consider all possible run-time subtypes.
Year
DOI
Venue
1995
10.1007/s002360050032
Acta Inf.
Keywords
Field
DocType
Data Structure,Communication Network,Information Theory,Computational Mathematic,Computer System
Functional verification,Formal language,Programming language,Computer science,Formal specification,Runtime verification,Theoretical computer science,Object language,Soundness,Formal methods,Formal verification
Journal
Volume
Issue
ISSN
32
8
0001-5903
Citations 
PageRank 
References 
41
2.67
32
Authors
2
Name
Order
Citations
PageRank
Gary T. Leavens12593211.29
William E. Weihl22614903.11