Přístupnostní navigace
E-přihláška
Vyhledávání Vyhledat Zavřít
Detail publikace
RYŠAVÝ, O.
Originální název
Inheritance of specifications in the calculus of functional objects
Typ
výzkumná zpráva
Jazyk
angličtina
Originální abstrakt
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.
Klíčová slova
Abstract data types, formal definitions and theory, object-oriented languages, object types, program construction, type theory.
Autoři
Rok RIV
2006
Vydáno
6. 10. 2006
Nakladatel
Faculty of Information Technology BUT
Místo
Brno
Strany počet
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" }