Groups | Search | Server Info | Keyboard shortcuts | Login | Register [http] [https] [nntp] [nntps]

Groups > comp.compilers > #2320

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

Show all headers | View raw

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

Back to comp.compilers | Previous | Next — Previous in thread | Next in thread | Find similar

Thread

At what point is a language so abstract that it simply cannot be compiled? "Costello, Roger L." <costello@mitre.org> - 2019-05-13 14:38 +0000
  Re: At what point is a language so abstract that it simply cannot be compiled? "Derek M. Jones" <derek@_NOSPAM_knosof.co.uk> - 2019-05-13 20:15 +0100
    Re: At what point is a language so abstract that it simply cannot be compiled? Jan Ziak <0xe2.0x9a.0x9b@gmail.com> - 2019-05-14 08:52 -0700
  Re: At what point is a language so abstract that it simply cannot be compiled? Martin Ward <martin@gkc.org.uk> - 2019-05-14 12:52 +0100
  Re: At what point is a language so abstract that it simply cannot be compiled? gah4@u.washington.edu - 2020-02-27 18:27 -0800

csiph-web