11
$\begingroup$

Is there any tool for prototyping a programming language semantics and type system and that also allows for some sort of model checking of standard properties, like type soundness?

I'm asking this, because I'm reading a book on Alloy and it provides the exact functionality that I want, but for models expressed using relational logic.

I'm aware of Ott, but it does not have this sort of "model checking" capability, since it is focused on generating code for proof assistant systems.

Any reference on such tool existence would be nice.

|cite|improve this question
$\endgroup$
  • 1
    $\begingroup$ Ott is step one, then you do the model checking in your favorite proof assistant. $\endgroup$ – Gilles 'SO- stop being evil' Nov 1 '16 at 21:57
  • $\begingroup$ @Gilles: Ok, but a point of a model checking tool is that it generates a whole set of elements of a given size in order to check if the property is indeed valid for them. In this way, I'll need to code this generation part for every language defined. Did you know if there's any way to automate this generation step? $\endgroup$ – Rodrigo Ribeiro Nov 3 '16 at 0:40
  • $\begingroup$ Technically, you can do this in a proof assistant (at least in one such as Coq) but it'll probably be very slow. Proof assistants are geared towards human-assisted proofs rather than automatically trying millions of ways to break the problem down. If you want to reuse Ott, you could add a backend for your favorite model checker. $\endgroup$ – Gilles 'SO- stop being evil' Nov 3 '16 at 0:43
8
$\begingroup$

Although there are frameworks created specifically for the purpose of prototyping programming languages (including their semantics, type systems, evaluation, as well as checking properties about them), the best choice depends on your particular case and specific needs.

Having that said, there are multiple (perhaps not so distinct) alternatives you might take (which includie the ones you've already mentioned):

  • using a specific language/framework designed for creating and prototyping new languages: as an example, Redex [1], a domain-specific language embedded in Racket for specifying and checking (operational) semantics of programming languages, which, given a definition of a language, provides easy handling of tasks such as typesetting (in Latex), inspecting traces of reduction, unit tests and random testing (e.g. for checking typing)
  • using general modelling languages that offer defining and performing certain analyses easily, as long as they can capture the specific language at hand to the needed extent; Alloy [2] is an example of such an approach: albeit pretty general and flexible, languages can be modelled as relations between states, while the support for model checking (e.g. evaluation within such language) comes for free after the semantics is expressed with a relation model (e.g. some ideas for modelling semantics of a language can be found in [3])
  • embedding the language to check its properties using a theorem prover; an example would defining the language as well as its semantics by embedding it in a proof system like Coq [4] (more details about this approach, as well as discussion and demonstration of the difference between deep and shallow embedding in Coq is given in [5])
  • using Ott (as already mentioned, with similar in spirit as Redex, but providing a new definition language rather than being embedded); Ott allows you to define the programming language in a convenient notation, and produce typesetting and definitions in a proof system (usually with deep embedding), where most of the checking (i.e. proof) needs to be performed manually
  • developing the language and its semantics, as well as appropriate checks (e.g. as tests) "from scratch" in a general-purpose programming language and translation into other systems if need be, for checking purposes (some languages, like Leon [6], include built-in verifiers, which allow automatically proving certain properties and make this approach similar to embedding in a proof system)

Note that there is the trade-off between how easy is to use the framework/tool (e.g. as easy as laying out the definition on paper or in Latex) and how powerful the mechanisms for checking the properties about the language are (e.g. embedding the language in a theorem prover can allow checking very elaborate properties).

[1] Casey Klein, John Clements, Christos Dimoulas, Carl Eastlund, Matthias Felleisen, Matthew Flatt, Jay A. McCarthy, Jon Rafkind, Sam Tobin-Hochstadt, and Robert Bruce Findler. Run Your Research: On the Effectiveness of Lightweight Mechanization. POPL, 2012.

[2] Daniel Jackson. Alloy: a lightweight object modelling notation. TOSEM, 2002.

[3] Greg Dennis, Felix Chang, Daniel Jackson. Modular Verification of Code with SAT. ISSTA, 2006

[4] Coq formal proof management system

[5] Formal Reasoning About Programs. Adam Chlipala, 2016

[6] Leon automated system for verifying, repairing, and synthesizing functional Scala programs

|cite|improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.