Nikolaj S. Bjørner
Kestrel Institute
3260 Hillview Avenue, CA 94304, USA
Fax: ++1 (650) 424-1807
bjorner@kestrel.edu
http://Theory.Stanford.EDU/people/nikolaj/
Abstract
Specware, Kestrel's specification tool draws concepts from category
theory, algebraic specification, software refinement, and program synthesis.
Unfortunately, in spite of an ample supply of foundation, it has not yet been
particularly helpful for writing specifications, refine these or even
execute these.
I will describe how some of the usability hurdles are overcome with slight
language-based modifications that have had dramatic benefits to ease of use,
and continue to describe the resulting impact on modeling Specware as a
software system structure using Specware.
Aside from this pragmatic approach to handling the software development
at Kestrel I will in a more technical part of the talk describe a type based
approach to statically check meta programs (programs that manipulate other
programs) for type correctness with respect to the object program
manipulations.
This investigation focuses on automatically validating the main activities of
the tools in Specware, namely program transformation.
Last Updated: May 22, 2000 by Elisabetta Ferrando