Paper Info
Title
Towards an Object-Oriented Progification Language
Abstract
To support formal verification of object-oriented programs we have proposed elsewhere an encoding in the type-theoretic proofchecker Lego. By treating programs and proofs uniformly, the encoding provides object-oriented proving principles — including inheritance of proofs — as analogues to object-oriented programming principles. Though the encoding is suitable for implementing ideas, it is not convenient for developing large verified programs. Here we propose a portmanteau language hopefully better suited to both ends: programming and verification. Although the language could be translated rigorously to -terms of the Lego-encoding we sketch the translation informally. We shall argue, along the way, that object-oriented verification can be regarded as a kind of generalized object-oriented programming.
Year
DOI
Venue
1997
10.1007/BFb0028396
TPHOLs
Keywords
Field
DocType
object-oriented progification language,object oriented,formal verification,object oriented programming
Functional logic programming,Programming language specification,Programming language,Object-oriented programming,Computer science,Inductive programming,Algorithm,Very high-level programming language,Theoretical computer science,First-generation programming language,Programming language implementation,Formal verification
Conference
ISBN
Citations 
PageRank 
3-540-63379-0
1
0.57
References 
Authors
6
1
Name
Order
Citations
PageRank
Wolfgang Naraschewski1577.89