Einträge mit dem Tag ‘Lox’

It has taken me some time, but I have pushed my lox-spark project one step further: the code is now complete up to the end of chapter 5 in Bob's book.

Why has this taken so long, even though the new code is still unproven (i.e. the proof hasn't progressed beyond chapter 4)?

The Visitor pattern turned out to be quite​ a nut to crack. Bob has used templated accept() methods. This means a concrete visitor can choose to return whatever type it needs -- the example AST printer returns a string, but later in the book, other types might come in handy. Unfortunately, in Ada generic functions cannot be overloaded, so I couldn't copy this approach. I tried to code around this restriction only to discover I didn't really understand the Visitor pattern (which I hadn't encountered before).

After some searching, I found an Ada implementation by Matthew Heaney. He, too​, uses generics, but in a different way. The gist is that instead of returning a value, the Visitor type ("object") stores the data internally -- this is not a problem because the abstract visitor type is extended (subclassed) anyway -- and can then be queried by the caller. There seems to be a bit more boilerplate code, but most of this is written by Lox's source code generator, so this is no real problem.

The second nut stems from a shortcoming in current prover technology: Gnatprove cannot deal with aliasing (i.e. writing to one variable changes the value of another), and therefore access variables (pointers) are not allowed in SPARK. This is not as large a problem as it may seem since Ada programmers use access variables very sparingly. But the abstract syntax tree has nodes containing other nodes, so some kind of reference is needed.

I have decided to store all Exprs in a Formal_Indefinite_Vector (a container supplied by the standard library) and refer to them by their index in the vector.

I am quite satisfied with how far lox-spark has come, this is a good way to start the weekend.

What's next? Obviously, the new code needs to be annotated and proven. Also, chapter six has been out for almost two weeks, so there's still more code to be written. I haven't yet decided on where to start, so maybe I'll take advantage of git and do both in parallel.

Kein Kommentar

My current pet project is coming along quite well: the implementation is complete up to chapter four (Scanning). More importantly, the AoRTE proof (absence of runtime errors) is also completely done. The only shortcomings are a handful of package bodies that are compiled with SPARK_mode => off: Ada.Command_Line and SPARK.Text_IO come to mind.

A few days ago, Bob has published the fifth chapter of his book. It is mainly about theory, and the only code it contains is a tool that generates source code for a part of the interpreter (the type hierarchy of the abstract syntax tree).

I thought about this for a while, and came to the conclusion I would not follow his path. Instead, I planned to write the types by hand. Here is why: generating source code is not really a problem, and since the generator would not be part of the final program, I would write it in plain Ada (without proving anything). The resulting code, however, would be part of the interpreter and thus needs to be proven. I could add the necessary annotations by hand, but that would defeat a big advantage of the generator: one can make changes at a high level (namely, change the input to the generator) and regenerate the sources. This is fine for ordinary languages, but it will kill my hand-written annotations.

Meanwhile, about a dozen Lox ports have appeared on github. I looked at all those I could find, but nobody seems to have written code related to the new chapter. Either the other developers have not yet found the time to implement the generator, or they, too, have their doubts.

Somehow, this lack of activity has prompted me to revise my decision: I will implement the generator, and I will generate annotations as well. After all, this project was meant to help me learn something new, and to be a challenge. But what good is a challenge unless it is challenging?

This should keep me busy in the coming days (I have not yet written any code for the generator). A quick Google search tells me that I can build multiple executables from the same project with GNAT, so that simplifies things on the organisational side.

Watch this site (or better yet, github) for updates!

Kein Kommentar

For some time, I've taken an interest in software engineering. With that, I mean robust software. After learning about Ada (my first project is from 2011), I haven't looked back (at C/C++, that is); Since then, I've learned a little about formal methods. So far, a few half-hearted attempts at SPARK/Ada have been the only results.

Now, I have stumbled across a project of Bob Nystrom's: He has designed a simple programming language, Lox, and is writing (and continuously publishing) a book on how to implement it. He has chosen Java and C, but quite a few folks have taken his code and re-implemented it in various languages: Alejandro Martinez (Swift), Ivan Katanic (C++), Paul Jackson (Go), Sasha Matijasic (Python).

So, why not do a SPARK port? I have some past experience with various parsers, so writing the bare code should not be that hard. Once that is done, annotations could be added and proofs done. The advantage of this project is that Bob is doing it now, chapter by chapter; I expect to follow at more or less the same pace, so if SPARKifying means I have to change something fundamental, I do not have to do that to the complete program. Instead, I can deal with problems as they crop up in the early stages.

I should add that SPARK can be used in different ways (or maybe I should say intensities). In the simplest case, only absence of runtime errors is proven. However, it is also possible to prove functional correctness at various levels: For example, one might set out to prove that a sorting subroutine actually returns a sorted list. This approach can be extended to more and more routines and eventually encompass the whole program. I do not know how far down this path I will (manage to) go, and in any case I have no idea how to prove functional correctness for a compiler.

Time will tell, I guess. Back to writing code now.

Kein Kommentar