CAMILA

A System for Software Development using Formal Methods

FAQ - Frequently Asked Questions

Mon Feb 17 12:00:00 MET 1997

Back to the CAMILA home page

CAMILA is a software development environment intended to promote the use of formal methods in industrial software environments.

It is currently being developed by JNICT consortium 169/90 (INESC group 2361 hosted by the University of Minho, Braga, Portugal, and the Department of Informatics of the same University) by a team led by Prof. José N. Oliveira.

Please send all your questions, comments and suggestions to the CAMILA mailing list: camila@di.uminho.pt

UNDER CONSTRUCTION!!!

Q1. Is there any version of CAMILA for MS-DOS (16bits)?

A1. Yes, there is. Please download the file camila-dos16.ZIP (~121Kb) and read the README file included in the package.

Q2. Is there any version of CAMILA for MS-DOS (32bits)?

A2. Yes, there is. Please download the file camila-dos32.ZIP (~178Kb) and read the README file included in the package.

Q3. Is there any version of CAMILA for LINUX?

A3. Yes, there is. Please download the file camila-linux.ZIP (~???) and read the README file included in the package.

Q4. How can I use the XMETOO DLL with Microsoft Visual C++ 4.0 (32 bits)?

A4. Please download the file xmetoo-dll32-test.ZIP (~34Kb) and execute the following commands:

1. Run Visual C++ 4.0

2. Click on File/Open Workspace menu option

3. Click on file app.mdb

4. Click on Insert/File into Project menu option

5. Click on src/app.c and lib/xmetoo.lib files

6. Click on Build/Build app.exe menu option

7. Copy the file xmetoo.dll to the \windows\system directory

8. Copy the file app.exe to the dlltest\bin directory

9. Run app.exe

;----------------------

;RSC-REPOSITORY FFUN/96

;----------------------

TYPE

S = A -> B;

A = ANY;

B = ANY;

ENDTYPE

FUNC INIT()

STATE S <- [];

FUNC INS(a:A,b:B)

PRE a notin dom(S)

STATE S <- S + [a->b];

FUNC REM(a:A)

STATE S <- S \ {a};

FUNC FIND(a:A):B

PRE a in dom(S)

RETURN S[a];

FUNC EMPTY():Bool

RETURN S == [];

#include <stdio.h>

#define XM95

#include "xmc.h"

SEXP f(SEXP s)

{

printf("Hello, I'm function f running...\n");

return NULL;

}

int main()

{ SEXP x; char *y[] = {"ffun.met"};

libxminit(1,y);

x = libxmevalstr("(add 2 3)");

xlsubr("fff",f);

x = libxmevalstr("(fff)");

printf("I'm back...\n");

x = libxmevalstr("(INIT)");

x = libxmevalstr("(INS \"a\" 1)");

x = libxmevalstr("(INS \"b\" 2)");

x = libxmevalstr("(pp S)");

return 1;

}

Q5. How can I use the XMETOO DLL with Microsoft Visual C++ 2.0 (16 bits)?

A5. Please download the file ............

Q6. How can I use the XMETOO DLL with Microsoft Visual Basic 4.0 (32 bits)?

A6. Please download the file xmetoo-dll32.ZIP (~77Kb) and extract the files in it.

Then put the file "xmetoo.dll" intothe \windows\system directory or in your project

directory. Download also the file camila-vb4.ZIP and extract the skeleton application

in it. Reuse it, see the source code or just run it!

Here is the source code of the XMETOO.BAS file (included in the package):

Global xmReturn As Integer

Global xmFilePointer As Long

Global xmResult As String * 1000

Declare Function xmInit Lib "xmetoo.dll" (ByVal xmFile As String) As Integer

Declare Function xmEval Lib "xmetoo.dll" (ByVal xmCmd As String, ByVal xmRes As String) As Integer

The variables above are used in the invocation of the functions. Here is an example:

xmReturn = xmInit("ffun.met")

xmReturn = xmEval("(INIT)", xmResult)

xmReturn = xmEval("(INS 1 'a)", xmResult)

xmReturn = xmEval("(FIND 1)", xmResult)

Q7. How can I use the XMETOO DLL with Microsoft Visual Basic 3.0 (16 bits)?

A7. Please download the file............

Q8. How can I use the XMETOO DLL with Borland Delphi (32 bits)?

A8. Please download the file xmetoo-dll32.ZIP (~77Kb) and extract the files in it.

Then put the file "xmetoo.dll" intothe \windows\system directory or in your project

directory. Download also the file camila-bd2.ZIP and extract the skeleton application

in it. Reuse it, see the source code or just run it!

Here is the source code of the XMETOO.PAS file (included in the package):

unit XMETOO;

interface

var

xmReturn:integer;

xmResult:array[0..100] of char;

function xmInit(xmFile:PChar): integer; stdcall; external 'xmetoo.dll';

function xmEval(xmIn:PChar; xmOut:PChar): integer; stdcall; external 'xmetoo.dll';

implementation

end.

The variables above are used in the invocation of the functions. Here is an example:

xmReturn := xmInit('ffun.met');

xmReturn := xmEval('(INIT)', xmResult);

xmReturn := xmEval('(INS 1 \'a)', xmResult);

xmReturn := xmEval('(FIND 1)', xmResult);

Q9. I am trying to use the XMETOO DLL with the STACK example from the book Systems Prototyping in Camila, but every time I execute the program (see the C source code bellow) the following message appears:

result for x:X :

where x:X is the argument of the function push.

; ---------- SORTS --------------------

TYPE

X = STR;

Stack = X-list;

ENDTYPE

; ---------- STATE --------------------

S : Stack;

; ---------- EVENTS -------------------

FUNC INIT():

STATE S <- <>;

FUNC PUSH(x:X):

STATE S <- <x:S>;

FUNC POP():X

PRE S != <>

RETURN head(S)

STATE S <- tail(S);

FUNC TOP():X

PRE S != <>

RETURN head(S);

char *argv[]={"stack.cam"};

#include <stdio.h>

#include "xmc.h"

#define INIT libxmeval (f0("INIT"))

#define PUSH(e) libxmeval (f1("PUSH",intsexp(e)))

#define POP libxmeval (f0("POP"))

#define TOP libxmeval (f0("TOP"))->n_int

main()

{SEXP N,aux,x,y,libxmevalstr(),libxmeval();

libxminit(1,argv);

INIT;

PUSH(8);

PUSH(7);

PUSH(6);

N=libxmevalstr("S ");

forall (aux,x,N) printf ("%d",x->n_int);

POP;

printf("\n%d\n",TOP);

N=libxmeval(symsexp("S"));

forall (aux,x,N) printf ("%d",x->n_int);

}

A9. In order to use the XMETOO DLL it is necessary to convert the CAMILA specification to XMETOO. For that use, for example, the command 'seca file.cam > file.met'. In that sense, the first line of C code bellow must be changed to:

char *argv[]={"stack.met"};

where "stack.met" is the file resulting from the execution of the command 'seca stack.cam > stack.met'.

Q10. ..........

A10. ..........

The CAMILA project has been funded by JNICT contract Ref. 169/90.