Technical report

RYŠAVÝ Ondřej. Inheritance of specifications in the calculus of functional objects. Brno: Faculty of Information Technology BUT, 2006.
Publication language:english
Original title:Inheritance of specifications in the calculus of functional objects
Title (cs):Dědičnost v jazyce kalkulu funkcionálních objektů
Pages:15
Place:Brno, CZ
Year:2006
Publisher:Faculty of Information Technology BUT
URL:http://www.fit.vutbr.cz/~rysavy/publications/rysavy_06_inheritance.pdf [PDF]
Keywords
Abstract data types, formal definitions and theory, object-oriented languages, object types, program construction, type theory.
Annotation
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.
BibTeX:
@TECHREPORT{
   author = {Ond{\v{r}}ej Ry{\v{s}}av{\'{y}}},
   title = {Inheritance of specifications in the calculus of
	functional objects},
   pages = {15},
   year = {2006},
   location = {Brno, CZ},
   publisher = {Faculty of Information Technology BUT},
   language = {english},
   url = {http://www.fit.vutbr.cz/research/view_pub.php?id=8185}
}

Your IPv4 address: 52.200.130.163
Switch to https