Index of /~mikon/Dijkstra

Name	Last modified	Size

Parent Directory		-
Abstractor/	2005-09-04 00:55	-
COPYING	1998-10-14 17:48	18K
Elaborator/	2005-09-04 00:55	-
Lexer/	2005-09-04 00:55	-
Linker/	2005-09-04 00:55	-
Parser/	2005-09-04 00:55	-
README.cockney	1998-10-14 17:48	5.1K
README.english	1998-10-14 17:48	4.9K
README.html	2011-01-23 19:15	5.9K
SemanticObjects/	2005-09-04 00:55	-
Test/	2005-09-04 00:55	-
build.sml	1998-10-14 17:48	3.8K
dij-sml-eml_1.1-2.tar.gz	1998-10-14 17:48	57K
dij/	2005-09-04 00:55	-
sources.cm	1998-10-14 17:48	3.1K
ver.EML.build.sml	1998-10-14 17:48	4.8K
ver.EML/	2005-08-08 18:09	-

A toy interpreter of the Dijkstra's language

This interpreter (compiler?) was written out of my fascination over
Edsger W. Dijkstra
"A discipline of programming"
Prentice-Hall, 1976.

The (dis)similarity of the implemented language to the one described in the book, can be estimated on the basis of examples contained in dij/ directory, the syntax described in Abstractor/ABSTRACT_GRAMMAR.sml file, and the denotational semantics residing in Elaborator/ directory.

Any decision of not keeping with the spirit of the original, in the design of the semantics, was heavily thought of:

the concurrent assignment is not implemented, because I have the feeling, that it's just a special case of pattern matching with product types, and so should be implemented in full generality (in the future versions, of course :) ,
the decision to move declaration of variable's type from virgin assignment to variable declaration itself, is due to the belief, that nothing gets lost, but the typing gets "stronger" and easier to read,
the if...fi and do...od constructs are made deterministic, to avoid artificial complexity. Still they do fulfill the requirements described in non-deterministic fashion in the book. But in fact, the non-deterministic notation seems to be very nice. It helps in manifesting, the independence from the guard evaluation order, which is quite common. This could also give optimizing compilers more freedom, although at the cost of the need for making separate binaries for testing, with run-time-random choosing of evaluation order.
the arrays are not implemented, although they can be simulated to some extent. Arrays have so imperative and simple nature, but on the other hand their proposed semantics was quite complicated and possessed no (apparent) imperative, efficient implementation. So, if not for the efficiency, what for?

The only ad hoc change to the original language was adding denotations of blocks to storable values, with block application, higher-order blocks, and such-like. This was needed for ad hoc input-output of programs, and for as hoc simulation of arrays. This doesn't seem to be a wild idea, or does it? Anyway, I tried to make a sound, elegant definition of blocks as values, I swear, I tried hard. No success :(. The final definition seems to be the most manageable of all, but even in this one blocks appearing as values posses an exotic, ugly, counter-intuitive and non-imperative feature, which is left as an exercise for the reader to find.

This project started in early 1994, after lectures about denotational semantics by Michal Grabowski and labs about implementing denotational semantics in Standard ML with Grzegorz Grudzinski (hi Grzes!). In these times, the author of the interpreter still had hopes, that imperative languages can be beautiful, and imperative programming - not error-provoking. To instantiate the hopes, or drop them once and for all, he decided to try to make a clean, mathematically beautiful, executable denotational definition of the most beautiful imperative language, possessing the most natural and the safest, bug-eliminating variable scoping mechanisms - the Dijkstra's language.

Any conclusions of this project are left, for an intrepid reader of SML sources, to draw :). Nevertheless, the fact is, that I'm quite satisfied with this work, done with the use of functional and specification languages. Also, this was quite thrilling to write, or even only rewrite, some sample programs in imperative language, after so many years ...

The interpreter was written in a functional programming language Standard ML to run on SML/NJ 109+. Versions 0.93-108 all crash in three places :-P.

The Lexer was written as a case study of developing software in Extended ML to run on EML Kit. File ver.EML.build.sml builds the EML version of the interpreter.

Here is the root of the source tree. The .tar.gz archive of the tree is available by WWW from
http://www.mimuw.edu.pl/~mikon/Dijkstra/dij-sml-eml_1.1-2.tar.gz
or by ftp from
ftp://www.mimuw.edu.pl/pub/mikon/Dijkstra/dij-sml-eml_1.1-2.tar.gz.

This program is free software; you can redistribute it and/or modify it under the terms of the GNU General Public License as published by the Free Software Foundation; either version 2 of the License, or (at your option) any later version.

This program is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU General Public License for more details.