|From:||Martin Ward <firstname.lastname@example.org>|
|Date:||Tue, 14 May 2019 12:52:44 +0100|
|Injection-Info:||gal.iecc.com; posting-host="news.iecc.com:2001:470:1f07:1126:0:676f:7373:6970"; logging-data="87760"; mail-complaints-to="email@example.com"|
|Posted-Date:||14 May 2019 12:57:53 EDT|
My WSL language is a "wide spectrum language" which includes
abstract specifications and low-level programming constructs in
the same language. At the specification level you can write
a specification statement of the form:
x := x'.Q
where x is a list of variable, x' is the corresponding list
of "primed variables" and Q is any formula of infinitary
first-order logic. If there is a set of values which can be assigned
to x' such that Q becomes true, then these values are assigned to x
and the statement terminates. (If there is more than one such
set of values, then one is selected nondeterminstically).
Otherwise, the statement aborts (does not terminate). For example:
<x> := <x'>.(x' = x + 1)
increments the value in x.
Since Q is a formula of infinitary first order logic,
the specification statement can be infinitely long.
There are formulae for which the solution cannot be computed:
for example, the Halting Problem for a Turing machine
can be implemented as a specification statement in WSL.
The language is used as the basis for my research into
program transformations. By using a wide-spectrum language
the refinement of a specification into exectuable code
is an example of a program transformation, as is the process
of reverse-engineering an abstract specification from
A subset of WSL (not including the specification statement)
is implemented in the FermaT program transformation system:
The FermaT program transformation system is used commercially
to migrate assembler code to structured and maintainable
functionally equivalent high-level language code.
This paper includes an introduction to WSL and transformation theory:
"Pigs from Sausages? Reengineering from Assembler to C via
FermaT Transformations", M.Ward, Science of Computer Programming,
Special Issue on Program Transformation,
Vol 52/1-3, pp 213-255, 2004. ISSN 0167-6423
This paper discusses how the theory can be used to derive
algorithms from specifications to give a provably correct
"Provably Correct Derivation of Algorithms Using FermaT"
Martin Ward and Hussein Zedan
Formal Aspects of Computing, Volume 26, Issue 5, Pages 993–1031,
September 2014, ISSN 0934-5043
Copies of these papers and others are available on my web site:
Dr Martin Ward | Email: firstname.lastname@example.org | http://www.gkc.org.uk
G.K.Chesterton site: http://www.gkc.org.uk/gkc | Erdos number: 4
Return to the
Search the comp.compilers archives again.