@incollection{Sekerinski96TypeTheoreticObjectOrientedRefinement,
	title = {A {Type}-{Theoretic} {Basis} for an {Object}-{Oriented} {Refinement} {Calculus}},
	url = {https://www.cas.mcmaster.ca/~emil/pubs/Sekerinski96TypeTheoreticObjectOrientedRefinement.pdf},
	abstract = {This paper addresses the issue of giving a formal semantics to an object-oriented programming and specification language. Object-oriented constructs considered are objects with attributes and methods, encapsulation of attributes, subtyping, bounded type parameters, classes, and inheritance. Classes are distinguished from object types. Besides usual imperative statements, specification statements are included. Specification statements allow changes of variables to be described by a predicate. They are abstract in the sense that they are non-executable. Specification statements may appear in method bodies of classes, leading to abstract classes. The motivation for this approach is that abstract classes can be used for problem-oriented specification in early stages and later refined to efficient implementations. Various refinement calculi provide laws for procedural and data refinement, which can be used here for class refinement. This paper, however, focuses on the semantics of object-oriented programs and specifications and gives some examples of abstract and concrete classes. The semantics is given by a translation of the constructs into the type system F≤, an extension of the simple typed λ-calculus by subtyping and parametric polymorphism: The state of a program is represented by a record. A state predicate is a Boolean valued function from states. Statements, both abstract and concrete, are represented by predicate transformers, i. e. higher order functions mapping state predicates (postconditions) to state predicates (preconditions). Objects are represented by records of statements (the methods) operating on a record of attributes, where the attributes are hidden by existential quantification. Classes are understood as templates for the creation of objects. Classes are represented by records. Inheritance amounts to record overwriting. Subtyping and parametric polymorphism, e. g. for the parameterization of classes by types, are already present in F≤. The advantage of this semantic by translation is that it builds on the features already provided by F≤ (which are all used). Hence no direct reference to the model underlying F≤ needs to be made; a summary of the syntax and rules of F≤ is given.},
	booktitle = {Formal {Methods} and {Object} {Technology}},
	publisher = {Springer-Verlag},
	author = {Sekerinski, Emil},
	editor = {Goldsack, Stephen J. and Kent, Stuart J. H.},
	year = {1996},
	doi = {10.1007/978-1-4471-3071-0_15},
	keywords = {10.1007/978-1-4471-3071-0\_15},
	pages = {317--335},
}

{"_id":"ZngGqpqCkncCaKB95","bibbaseid":"sekerinski-atypetheoreticbasisforanobjectorientedrefinementcalculus-1996","author_short":["Sekerinski, E."],"bibdata":{"bibtype":"incollection","type":"incollection","title":"A Type-Theoretic Basis for an Object-Oriented Refinement Calculus","url":"https://www.cas.mcmaster.ca/~emil/pubs/Sekerinski96TypeTheoreticObjectOrientedRefinement.pdf","abstract":"This paper addresses the issue of giving a formal semantics to an object-oriented programming and specification language. Object-oriented constructs considered are objects with attributes and methods, encapsulation of attributes, subtyping, bounded type parameters, classes, and inheritance. Classes are distinguished from object types. Besides usual imperative statements, specification statements are included. Specification statements allow changes of variables to be described by a predicate. They are abstract in the sense that they are non-executable. Specification statements may appear in method bodies of classes, leading to abstract classes. The motivation for this approach is that abstract classes can be used for problem-oriented specification in early stages and later refined to efficient implementations. Various refinement calculi provide laws for procedural and data refinement, which can be used here for class refinement. This paper, however, focuses on the semantics of object-oriented programs and specifications and gives some examples of abstract and concrete classes. The semantics is given by a translation of the constructs into the type system F≤, an extension of the simple typed λ-calculus by subtyping and parametric polymorphism: The state of a program is represented by a record. A state predicate is a Boolean valued function from states. Statements, both abstract and concrete, are represented by predicate transformers, i. e. higher order functions mapping state predicates (postconditions) to state predicates (preconditions). Objects are represented by records of statements (the methods) operating on a record of attributes, where the attributes are hidden by existential quantification. Classes are understood as templates for the creation of objects. Classes are represented by records. Inheritance amounts to record overwriting. Subtyping and parametric polymorphism, e. g. for the parameterization of classes by types, are already present in F≤. The advantage of this semantic by translation is that it builds on the features already provided by F≤ (which are all used). Hence no direct reference to the model underlying F≤ needs to be made; a summary of the syntax and rules of F≤ is given.","booktitle":"Formal Methods and Object Technology","publisher":"Springer-Verlag","author":[{"propositions":[],"lastnames":["Sekerinski"],"firstnames":["Emil"],"suffixes":[]}],"editor":[{"propositions":[],"lastnames":["Goldsack"],"firstnames":["Stephen","J."],"suffixes":[]},{"propositions":[],"lastnames":["Kent"],"firstnames":["Stuart","J.","H."],"suffixes":[]}],"year":"1996","doi":"10.1007/978-1-4471-3071-0_15","keywords":"10.1007/978-1-4471-3071-0_15","pages":"317–335","bibtex":"@incollection{Sekerinski96TypeTheoreticObjectOrientedRefinement,\n\ttitle = {A {Type}-{Theoretic} {Basis} for an {Object}-{Oriented} {Refinement} {Calculus}},\n\turl = {https://www.cas.mcmaster.ca/~emil/pubs/Sekerinski96TypeTheoreticObjectOrientedRefinement.pdf},\n\tabstract = {This paper addresses the issue of giving a formal semantics to an object-oriented programming and specification language. Object-oriented constructs considered are objects with attributes and methods, encapsulation of attributes, subtyping, bounded type parameters, classes, and inheritance. Classes are distinguished from object types. Besides usual imperative statements, specification statements are included. Specification statements allow changes of variables to be described by a predicate. They are abstract in the sense that they are non-executable. Specification statements may appear in method bodies of classes, leading to abstract classes. The motivation for this approach is that abstract classes can be used for problem-oriented specification in early stages and later refined to efficient implementations. Various refinement calculi provide laws for procedural and data refinement, which can be used here for class refinement. This paper, however, focuses on the semantics of object-oriented programs and specifications and gives some examples of abstract and concrete classes. The semantics is given by a translation of the constructs into the type system F≤, an extension of the simple typed λ-calculus by subtyping and parametric polymorphism: The state of a program is represented by a record. A state predicate is a Boolean valued function from states. Statements, both abstract and concrete, are represented by predicate transformers, i. e. higher order functions mapping state predicates (postconditions) to state predicates (preconditions). Objects are represented by records of statements (the methods) operating on a record of attributes, where the attributes are hidden by existential quantification. Classes are understood as templates for the creation of objects. Classes are represented by records. Inheritance amounts to record overwriting. Subtyping and parametric polymorphism, e. g. for the parameterization of classes by types, are already present in F≤. The advantage of this semantic by translation is that it builds on the features already provided by F≤ (which are all used). Hence no direct reference to the model underlying F≤ needs to be made; a summary of the syntax and rules of F≤ is given.},\n\tbooktitle = {Formal {Methods} and {Object} {Technology}},\n\tpublisher = {Springer-Verlag},\n\tauthor = {Sekerinski, Emil},\n\teditor = {Goldsack, Stephen J. and Kent, Stuart J. H.},\n\tyear = {1996},\n\tdoi = {10.1007/978-1-4471-3071-0_15},\n\tkeywords = {10.1007/978-1-4471-3071-0\\_15},\n\tpages = {317--335},\n}\n\n","author_short":["Sekerinski, E."],"editor_short":["Goldsack, S. J.","Kent, S. J. H."],"key":"Sekerinski96TypeTheoreticObjectOrientedRefinement","id":"Sekerinski96TypeTheoreticObjectOrientedRefinement","bibbaseid":"sekerinski-atypetheoreticbasisforanobjectorientedrefinementcalculus-1996","role":"author","urls":{"Paper":"https://www.cas.mcmaster.ca/~emil/pubs/Sekerinski96TypeTheoreticObjectOrientedRefinement.pdf"},"keyword":["10.1007/978-1-4471-3071-0_15"],"metadata":{"authorlinks":{}}},"bibtype":"incollection","biburl":"https://api.krunk.cn/emil/bib.php","dataSources":["HEdahWqKBpmSGmDwq","MF5eGzpJnqf6bSAoG","TrZoiqc8JG7hqAynN","ienufKdnmJs49AsjR","pKojZwgcmAbzT5ufq","So4gmSWFmbQRNEuFs","yBNL6zg4bd77wFNse","CvQYP6Tmpapx74Mgr","RWydLHbBJqgdeh5jr"],"keywords":["10.1007/978-1-4471-3071-0_15"],"search_terms":["type","theoretic","basis","object","oriented","refinement","calculus","sekerinski"],"title":"A Type-Theoretic Basis for an Object-Oriented Refinement Calculus","year":1996}