archives

Formal Semantics and Soundness of an Algorithm for Translating Model-based Specifications to Concurrent Constraint Programs


Home 

About 

Browse 

Search 

Register 

Subscriptions 

Deposit Papers 

Help
    

Wahls, Tim and Leavens, Gary T. (2000) Formal Semantics and Soundness of an Algorithm for Translating Model-based Specifications to Concurrent Constraint Programs. Technical Report TR00-02a, Department of Computer Science, Iowa State University.

Full text available as:Postscript

Abstract

Formal Semantics and Soundness of an Algorithm for Translating
Model-based Specifications to Concurrent Constraint Programs
by
Tim Wahls and Gary T. Leavens
Abstract
This paper presents an algorithm for executing formal specifications,
and a proof of the soundness of that algorithm.  The algorithm
executes specifications written in the model-based specification
language SPECS-C++ by transforming such specifications to concurrent
constraint programs.  This approach can execute specifications written
at a high level of abstraction.  Denotational semantics techniques are
used for both explaining the algorithm and for proving its soundness.
Keywords: Executable specifications, behavioral interface
specification language, formal specification, prototyping, translation
of specifications to constraints, constraint programming, soundness,
denotational semantics, model-based specification, formal methods,
precondition, postcondition, SPECS-C++.
1999 CR Categories:
D.2.1 [Software Engineering] Requirements/Specifications
--- Rapid prototyping, languages, theory, tools;
D.2.4 [Software Engineering] Software/Program Verification
--- Formal methods, programming by contract, reliability, tools,
SPECS-C++;
D.2.7 [Software Engineering] Distribution, Maintenance, and Enhancement
--- Documentation;
D.3.2 [Programming Languages] Language Classifications
--- Constraint and logic languages,
nonprocedural languages, very high-level languages;
F.3.1 [Logics and Meanings of Programs]
Specifying and Verifying and Reasoning about Programs ---
Assertions, pre- and post-conditions,
specification techniques;
F.3.1 [Logics and Meanings of Programs] Semantics of Programming Languages
--- Denotational semantics.
Copyright (c) 2000 by Tim Wahls and Gary T. Leavens.

Subjects:All uncategorized technical reports
ID code:00000230
Deposited by:Staff Account on 24 August 2000



Contact site administrator at: ssg@cs.iastate.edu