Content area

Abstract

We present a formal semantics for an object-oriented specification language. The formal semantics is presented as a conservative shallow embedding in Isabelle/hol and the language is oriented towards ocl formulae in the context of uml class diagrams. On this basis, we formally derive several equational and tableaux calculi, which form the basis of an integrated proof environment including automatic proof support and support for the analysis of this type of specifications. We show applications of our proof environment to data refinement based on an adapted standard refinement notion. Thus, we provide an integrated formal method for refinement-based object-oriented development. [PUBLICATION ABSTRACT]

Details

10000008
Business indexing term
Title
Semantics, calculi, and analysis for object-oriented specifications
Publication title
Acta Informatica; Heidelberg
Volume
46
Issue
4
Pages
255-284
Number of pages
30
Publication year
2009
Publication date
Jul 2009
Publisher
Springer Nature B.V.
Place of publication
Heidelberg
Country of publication
Netherlands
ISSN
00015903
e-ISSN
14320525
CODEN
AINFA2
Source type
Scholarly Journal
Language of publication
English
Document type
Feature
ProQuest document ID
274958712
Document URL
https://www.proquest.com/scholarly-journals/semantics-calculi-analysis-object-oriented/docview/274958712/se-2?accountid=208611
Copyright
Springer-Verlag 2009
Last updated
2024-12-01
Database
ProQuest One Academic