Validated Prolog Compilers

Appeared in Volume 7/3, August 1994

Keywords: compilers.


ptb@cs.fit.edu 
Peter T. Breuer
4th April 1994

Does anybody know if there are any validated prolog compilers out there?

I'm happy to extend the question to include interpreters. Sure I understand that its easy to write a Prolog interpreter, and all the semantics work tells me what it means if I get an answer to a question against a rule base, but that doesn't make any particular implementation validated.

I'm asking because the lack of validated compilers was recently put to me as a reason why industry is still not taking much interest in Prolog for production work, despite its several advantages.

I know about the validation theory for Prolog programs from Antoy and Gannon.


ok@goanna.cs.rmit.oz.au 
Richard A. O'Keefe
8th April 1994

What do you mean by "validated"? In the commercial compiler world, a "validated" compiler is one which has passed some official test (there are validation suites for Fortran, COBOL, Pascal, and Ada that I know of, there may be more).

Since the ISO Prolog standard is not yet official, there can be no official validation suite for it, so there can be no validated compilers.

If you mean "verified", as in "there is a convincing formal or semi-formal argument that the compiler is correct with respect to a comprehensible specification", then the only non-trivial language for which I know of any verified compiler is Scheme (I have the reports which describe the proof and believe me, it wasn't easy). So the argument:

He wrote:

I'm asking because the lack of validated compilers was recently put to me as a reason why industry is still not taking much interest in Prolog for production work, despite its several advantages.

This strikes me as bogus. Industry is happily jumping on the C++ bandwagon, braying loudly, and if there is a C++ compiler that is validated in any sense, I would like to know about it. My friends who do serious work with C++ keep on complaining to me about serious bugs in the compilers they use.


rss@seg.npl.co.uk 
Roger Scowen
13th April 1994

A vote on a draft International Standard Prolog will be held from June-September 1994. This is the final phase in the standardization process and, if successful, a standard should be published early next year.

While the international standard for Prolog was being defined, Expert Systems Ltd developed a validation suite. Standardization has taken longer than hoped, and the suite is currently frozen. However it may be revised to be compatible with the eventual ISO standard Prolog, and BSI-QA (British Standards Institution - Quality Assurance Division) may offer a validation service for processors conforming to the standard.


ptb@dit.upm.es
Peter T. Breuer
27th June 1994

By "valid" I mean "proved correct", although I accept that the industrial version of the term is important.

I was at ICLP94 ("Proving Hardware Designs") and had the opportunity to talk to Stephan Diehl ("Towards a verified OR-parallel WAM"). He said that only in the last couple of years had there been any real proofs (by Russinoff) that compilation of Prolog for the WAM is correct. Stephan's own thesis is an effort at an OR-parallel extension.

Jeanette Wing also argued at ICLP that Prolog programers need to give some guarantees about non-functional measures, such as speed, before they will be able to persuade management to accept Prolog. I argued that they really need to offer more basic non-functional guarantees. Namely that their program will scale from 10 data items to 10000 without going quadratic or exponential. Geraint Wiggins argued that this was within the reach of current automatic proof assistants.

The work I referred to above is:

Antoy & Gannon, "Axiomatic Verification of Logic Programs", TR 90-26.1, Dept. of Comp. Sci., Portland State Univ. School of Engineering and Applied Sciences, PO Box 751, Portland OR 97207-0751, USA, Email: antoy@cs.pdx.edu, gannon@cs.umd.edu

Recent work by Boerger at Pisa has expressed Prolog implementations in "evolving algebras", but it looks very operational to me, and I get no insight from reading the work. Just the description of an arbitrary languages operational semantics written down algebraically, and specialised to Prolog. For example, see:

Bierle and Boerger, "Correctness proof for the WAM with types", In "Computer Science Logic - CSL/91", LNCS, Boerger, Jaeger, Buening and Richter (Eds), Email: boerger@dipisa.di.unip.it.