Publication detail

Inheritance of specifications in the calculus of functional objects

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

RYŠAVÝ, O.

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"
}