Formal Semantics and Soundness of an Algorithm

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.

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