Re: At what point is a language so abstract that it simply cannot be compiled?

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
executable code.


A subset of WSL (not including the specification statement)
is implemented in the FermaT program transformation system:


http://www.gkc.org.uk/fermat.html


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
doi:dx.doi.org/10.1016/j.scico.2004.03.007


This paper discusses how the theory can be used to derive
algorithms from specifications to give a provably correct
implementation:


"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
doi:10.1007/s00165-013-0287-2


Copies of these papers and others are available on my web site:


http://www.gkc.org.uk/martin/papers/index.html


--
Martin


Dr Martin Ward | Email: martin@gkc.org.uk | http://www.gkc.org.uk
G.K.Chesterton site: http://www.gkc.org.uk/gkc | Erdos number: 4

Return to the comp.compilers page.
Search the comp.compilers archives again.