Download ASLan++ specification and tutorial

D2.3 (update): ASLan++ specification and tutorial
specification U n i n i t i a l i z e d _ U n s a f e
channel_model CCM
entity Environment
{
symbols
uninitial ized_m sg ( message
): fact ;
uninitial ized_s et ( message set ): fact ;
symbols
UA : agent ;
UM : message ;
UK : symmetric_key ;
UN : nat ;
UP : public_key ;
US : private_key ;
UT : text ;
SA :
SM :
SK :
SN :
SP :
SS :
ST :
agent set ;
message set ;
symmetric_key set ;
nat set ;
public_key set ;
private_key set ;
text set ;
entity Test { % implicit Actor parameter not initialized !
symbols
U : message ;
S : message set ;
body {
send (i , U );
% sends an uninitialized msg variable !
S - > add ( i );
% uses an uninitialized set variable !
S := {};
% initializes the set variable
S - > add ( U );
% adds an uninitialized msg variable !
}
}
body
{
uninitial ized_m sg ( UA );
uninitial ized_m sg ( UM );
uninitial ized_m sg ( UK );
uninitial ized_m sg ( UN );
uninitial ized_m sg ( UP );
uninitial ized_m sg ( US );
uni nitia lized_ set ( SA );
uni nitia lized_ set ( SM );
uni nitia lized_ set ( SK );
uni nitia lized_ set ( SN );
uni nitia lized_ set ( SP );
uni nitia lized_ set ( SS );
FP7-ICT-2007-1
Project No. 216471
39/190