archives

Formal Semantics and Soundness of an Algorithm


Home 

About 

Browse 

Search 

Register 

Subscriptions 

Deposit Papers 

Help
    

Wahls, Tim and Leavens, Gary T. (2000) Formal Semantics and Soundness of an Algorithm. Technical Report TR00-02, Department of Computer Science, Iowa State University.

Full text available as:Postscript
Adobe PDF

Abstract

Formal Semantics and Soundness of an Algorithm
for Translating Model-based Specifications to 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 constraint
programs.  The generated programs use constraint satisfaction
techniques to 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:00000211
Deposited by:Staff Account on 10 March 2000



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