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.
The Camila revival project is being developed in distinct phases, which are briefly described below.
Phase I (Camila Revival)
Prototype camila interpreter in Haskell
Camila Prelude modules in Haskell
Both deliverables are integrated into the UMinho Haskell Software distribution.
"PURe CAMILA: A system for software development using formal methods" - Alexandra Mendes and Joćo Ferreira, LabMF 2005 - (Report) (Slides)
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:
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
This report explains how to mimic VDM++ features (parallelism not included) in Haskell.
Phase III (Camila enriched with components)
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: