Program Understanding and Re-engineering: Calculi and Applications




Sep 18 Paper Towards a Coordination Model for Interactive Systems by MarcoAntonioBarbosa, JoseCampos and LuisSoaresBarbosa has been accepted for FMIS'06 (Macau).

July 3 Paper Configurations of Web Services by MarcoAntonioBarbosa and LuisSoaresBarbosa has been accepted for FOCLASA'06 (Bonn, Germany).

July 3 Paper Strong Types for Relational Databases by Alexandra Silva and JoostVisser has been accepted for the Haskell Workshop 2006 (Portland, USA).

June 16 Paper Strongly Typed Rewriting For Coupled Software Transformation (by AlcinoCunha and JoostVisser) accepted by RULE 2006 (Seattle, USA).

May, 26 Paper Transposing Partial Coalgebras (by LuisSoaresBarbosa and JoseNunoOliveira) accepted for publication in TCS, Elsevier.

May, 11 Papers Type-safe two-level data transformation (by AlcinoCunha, JoseNunoOliveira and JoostVisser) and Pointfree factorization of operation refinement (by JoseNunoOliveira and Cesar Rodrigues) have been accepted by FM'06 (Canada).

May, 8 A paper entitled An Orchestrator for Dynamic Interconnection of Software Components, by MarcoAntonioBarbosa and LuisSoaresBarbosa, accepted at MTCoord'06 (Bologna).


Research » PURe » Camila

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.


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:
    • 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


Phase III (Camila enriched with components)

(to appear)


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:


Related Links

r15 - 04 Nov 2007 - 18:58:50 - JoseBacelarAlmeida
This site is powered by the TWiki collaboration platform Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.
Syndicate this site RSSATOM