Semantics Page

From Wiki.overturetool.org

Jump to: navigation, search

The aim of semantics research is to develop a formal semantics, broadly accepted by the community, that covers the VDM core as well as its extensions including object-oriented structuring, concurrency, time and distribution present in the language extensions.

Contents

State of the Art

There is a denotational semantics (in the ISO Standard), a proof theory (in Bicarregui et al.) and an operational semantics (in VDMTools and VDMJ) for VDM-SL. The work on VDM-SL identified challenges in coping with aspects such as looseness in the proof theory. For VDM++, we still lack a widely accepted semantics that deals with the object-oriented structuring and concurrency present in the language extensions. For VDM-RT, a starting point for semantics exists in the work of Verhoef and Hooman. The DESTECS project will support the development of a basic semantics of co-simulation.

A complete semantic definition for VDM++ and VDM-RT is important for the development of a consistent set of tools, so we propose an effort to produce a semantic definition of a unified VDM language which we will refer to as TR-001: VDM-10 Language Manual, P. G. Larsen, K. G. Lausdahl, N. Battle, and J. S. Fitzgerald, version 2, February 2011.

Background

This page summarises the state of the art in VDM semantics. It has been updated following the 8th Overture Workshop.

VDM-10 encompasses models which may be expressed in one of three styles -- plain specification (VDM-SL), object-oriented (VDM++), or real-time (VDM-RT). Each style is more structured and uses a richer modelling language than its predecessor. VDM-10 encompasses all three styles through designated language subsets

  • Specification Style is supported by the VDM-SL subset. Specification-style models are based on operations that modify global state. VDM-SL models may be structured using a module construct.
  • Object-Oriented Style is supported by the VDM++ subset. O-O models are structured by means of class definitions, in which functionality is described by operations that modify instance variables.
  • Real-Time Style extends the object-oriented style with features that allow the description of timed processes deployed onto communicating virtual CPUs.

The only VDM-10 definition to date is:

The following sources are mostly informal:

  • The VDM test suite (all dialects and aspects)
  • The VDM examples collection VDM Examples (for clean type-checked examples in VDM-SL, VDM++ and VDM-RT respectively)

VDM-SL Semantics

Starting Points

Aside from the VDM-10 Manual, the ISO Standard for VDM-SL gives denotational semantics for a language subset. Features of the full language are translated into the subset "before" the denotation is calculated.

  • Information technology -- Programming languages, their environments and system software interfaces -- Vienna Development Method -- Specification Language -- Part 1: Base language, International Standard ISO/IEC 13817-1, December 1996. A Leicester University technical report describing the standard in detail is available. (Techninal report with the VDM-SL semantics in pdf format). Contact is Derek Andrews (derek.andrews@yahoo.com).

The [[ProofBook][Proof in VDM]] Book proposes a logical frame and a proof theory for a large part of the -SL language, given in typed LPF. The logic used allows us to address undefinedness more cleanly than classical logics, but therefore does not correspond to what the tools currently do in their operational semantics. It does not give full axiomatisations of some parts of the language that have awkward semantics in the logical frame proposed. It also avoids explicit operations. John Fitzgerald's work proposes a proof-theoretic semantics for modules in -SL:

Peter Gorm Larsen's PhD thesis proposes proof rules for some aspects of -SL that were missing from the Proof in VDM work:

  • Peter Gorm Larsen, Towards Proof Rules for VDM-SL, PhD Thesis, Department of Computer Science, Technical University of Denmark, 1995. ID-TR:1995-160

Other starting points are:

  • The BSI grammar from Jones90
  • The CSK Language Manuals (grammar, and informal semantics)
  • The Modelling Systems Book (general informal semantics)

Open Issues

  • Detailed operation of module scoping and import/exports
  • Proof Theory covering the full base language

VDM++ Semantics

Starting Points

Other starting points are:

Open Issues

  • The extension of the SL type model to object oriented types
  • The complete set of POs for the language
  • Proof Theory

The 8th Overture Workshop began an initiative to develop a simple object-oriented core language (VDMCore) into which o-o models might be translated, and to give a simple semantcs to this. This reflects the approach taken in the flat language semantics. The following subtasks are being undertaken:

  • Semantics Definition. Team: John Fitzgerald, Peter Gorm Larsen, Erik Ernst, Ken Pierce, Joey Coleman (review), Cliff Jones (review)
  • Define CAS: Peter Gorm Larsen, Erik Ernst, John Fitzgerald, Nick Battle, Ken Pierce, Joey Coleman (review)
  • Explore Examples: Peter Gorm Larsen, Erik Ernst, Ken Pierce, Nick Battle, Leo Freitas
  • Syntactic Sugaring of VDMCore: Marcel Verhoef
  • Model Statistics: Nick Battle (tool)

VDM-RT Semantics

Starting Points

Marcel Verhoef. Modeling and Validating Distributed Embedded Real-Time Systems, PhD thesis, Radboud University Nijmegen, 21 January 2009 (Chapters 3 and 4 describe some of the syntax and semantics for real-time distributed extensions of VDM and also the CT/DE co-simulation. This thesis gives a more complete than the earlier papers presented at FM'06 and IFM'07)

The extensions for distribution and relative time on resources are also summarized in the recent festschrift paper, see

Jozef Hooman, Marcel Verhoef. Formal Semantics of a VDM Extension for Distributed Embedded Systems, D. Dams and U. Hannemann and M. Steffen (eds): W.P. de Roever Festschrift, LNCS 5930, pp 142-161, 2010 Author preprint

Open issues:

  • The complete set of POs for the language
  • The (very) fine detail of VDM-RT timing behaviour
Retrieved from "http://wiki.overturetool.org/index.php/Semantics_Page"
Personal tools