Sciweavers

Free Online Productivity Tools i2Speak i2Symbol i2OCR iTex2Img iWeb2Print iWeb2Shot i2Type iPdf2Split iPdf2Merge i2Bopomofo i2Arabic i2Style i2Image i2PDF iLatex2Rtf Sci2ools

14

FMOODS
2003

favoriteEmaildiscussreport

151views Formal Methods» more FMOODS 2003»

A Syntax-Directed Hoare Logic for Object-Oriented Programming Concepts

13 years 5 months ago

A Syntax-Directed Hoare Logic for Object-Oriented Programming Concepts

Download www.cs.uu.nl

This paper outlines a sound and complete Hoare logic for a sequential object-oriented language with inheritance and subtyping like Java. It describes a weakest precondition calculus for assignments and object-creation, as well as Hoare rules for reasoning about (mutually recursive) method invocations with dynamic binding. Our approach enasoning at an abstraction level that coincides with the general ion level of object-oriented languages.

Cees Pierik, Frank S. de Boer

Real-time Traffic

Complete Hoare Logic | FMOODS 2003 | FMOODS 2007 | Object-oriented Languages | Weakest Precondition Calculus |

claim paper

Related Content

» A Relational Model for ObjectOriented Designs

» A Logic of ObjectOriented Programs

» An Open System Operational Semantics for an ObjectOriented and ComponentBased Language

» Extensible Universes for ObjectOriented Data Models

» ObjectOriented Parallelisation of Java Desktop Programs

» A Logic Framework for a Semantics of ObjectOriented Data Modeling

» Chisel constructing hardware in a Scala embedded language

» Nested interpolants

» Algebra of Logic Programming

Post Info
More Details (n/a)

Added	31 Oct 2010
Updated	31 Oct 2010
Type	Conference
Year	2003
Where	FMOODS
Authors	Cees Pierik, Frank S. de Boer

Comments (0)