Přístupnostní navigace
E-application
Search Search Close
Publication detail
RYŠAVÝ, O.
Original Title
Inheritance of specifications in the calculus of functional objects
Type
report
Language
English
Original Abstract
Solid theoretical foundation of object-oriented paradigm have been developed for both functional and imperative programming languages. Although type theory contains functional programming language and offers rich specification and reasoning capabilities the similar foundation is not so evident despite the presence of flavor of object orientation in many other formal methods. The idea of the present work is straightforward. Object type consists of object's interface signature specification and accompanied specification in form of logical proposition. An object value is a collection of operations working on an internal state and a proof of correctness of the implementation. In this manner, certain principles of object-orientation can be also applied to accompanied proofs, namely inheritance, late binding, and encapsulation. Paper introduces a new calculus that features object notion as a primitive construction allowing for quite simple presentation. Object type constructor combines existential and recursive types akin to Self type of Abadi and Cardelli. To simplify the presentation and to avoid introducing general fixed point constructor a special sort of expressions is introduced -- boxed expressions. A boxed expression is an expression annotated with a variable that with suitable defined substitution operation allows us to encode a restricted form of self application and positive methods.
Keywords
Abstract data types, formal definitions and theory, object-oriented languages, object types, program construction, type theory.
Authors
RIV year
2006
Released
6. 10. 2006
Publisher
Faculty of Information Technology BUT
Location
Brno
Pages count
15
URL
http://www.fit.vutbr.cz/~rysavy/publications/rysavy_06_inheritance.pdf
BibTex
@techreport{BUT58318, author="Ondřej {Ryšavý}", title="Inheritance of specifications in the calculus of functional objects", year="2006", publisher="Faculty of Information Technology BUT", address="Brno", pages="15", url="http://www.fit.vutbr.cz/~rysavy/publications/rysavy_06_inheritance.pdf" }