CAMILA: VDM meets Haskell

The Camila project explores how concepts from the VDM specification language and the functional programming language Haskell can be combined. On the one hand, it includes experiments of expressing VDM's data types (e.g. maps, sets, sequences), data type invariants, pre- and post-conditions, and such within the Haskell language. On the other hand, it includes the translation of VDM specifications into Haskell programs.

This is a continuation (or revival) of the original Camila system, see http://camila.di.uminho.pt.

Overview

The Camila revival project is being developed in distinct phases, which are briefly described below.

Phase I (Camila Revival)

Deliverables:

  • Prototype camila interpreter in Haskell
  • Camila Prelude modules in Haskell

Both deliverables are integrated into the UMinho Haskell Software distribution.

Documents

  • "PURe CAMILA: A system for software development using formal methods" - Alexandra Mendes and João Ferreira, LabMF 2005 - (Report) (Slides)

Examples

In directory Camila/Examples you will find some examples (if you intend to add examples, you sould put them in this directory too). Before loading them in the interpreter, you will need to compile it. For example, to use the example Folder:

  • From libraries directory, run ghc --make Camila/Examples/Folder.hs -package plugins

  • From tools/Camila directory and after compiling the interpreter:
    • make run
    • :l Camila.Examples.Folder
    • create f := new Folder
    • eval f opread

(If you want to see more examples, please see Report -- Chapter 5 )

Phase II (VDM++ features)

VDM++, in comparison with VDM has the following extra features:

  • Allows the definition of classes and objects
  • Inheritance (specialization and generalization)
  • Operations and functions to describe functional behaviour of the objects
  • Threads and synchronisation constraints

Documents

Phase III (Camila enriched with components)

(to appear)

Downloads

You can find the latest version of CAMILA in Research.PURe CVS (see PUReSoftware). You will need hs-plugins package.

To use the prototype interpreter, you have to compile it (just run make in directory tools/Camila) -- don't forget you need to install hs-plugins package before doing this. To run it just do make run.

Note: At the moment, you will have to compile all the examples you want to run. (All these steps will be simplified in the future, so stay tuned)

A stand-alone release is also available:

Contributors

Related Links