1. kísérlet: Programozási tételek beépítése. A másolás tétele (CopyPrTh)…
instantiations
sorozat as CopyPrTh(nat,nat)
types
elem_1,
elem_2
functions
f: elem_1 -> elem_2
definitions
functions
masolas: seq of nat -> seq of nat
masolas(X)
== copy(X);
2. kísérlet: Programozási tételek definiálása VDM modulként. A másolás tétel
(CopyPrTh)…
1 module CopyPrTh
2 parameters
3 types
4 elem_1,
5 elem_2
6 functions
7 f: elem_1 -> elem_2
8 exports
9 all
10 definitions
11 functions
12 copy(X: seq of elem_1) Y:seq of elem_2
13 post forall i in set inds X & Y(i)=f(X(i));
14 end CopyPrTh
Az ún. flat VDM-SL-ben jó lenne az alábbi generic megfogalmazás is, de ez nem megy az IFAD-VDM-ben:
copyPrTh[@elem_1,@elem_2] (X: seq of elem_1) Y:seq of elem_2
pre elemenkentFeldolgozhato(f)
post forall i in set inds X & Y(i)=f(X(i));
Az alábbiakat az IFAD-VDM generálta C++ kódban a fenti modulhoz:
//
// THIS FILE IS AUTOMATICALLY GENERATED!!
//
// Generated at by the VDM-SLtoC++ Code Generator
//
// Supported compiler: g++ version 2.7.2
//
#include "CopyPrTh.h"
#include "vdm_CopyPrTh_implicit.cc"
void init_CopyPrTh() {} [modulnév:1
Bool vdm_CopyPrTh_post_copy(Sequence vdm_CopyPrTh_X, Sequence vdm_CopyPrTh_Y) { [művelet…:12
Bool varRes_4;
bool tmpQuant_5 = true;
{
bool succ_14 = true;
Set e_set_15; [‘set inds X’ halmaz generálásának kezdete
Set riseq_17;
int max_18 = (Int) vdm_CopyPrTh_X.Length(); [13
for (int i_19 = 1; i_19 <= max_18; i_19++)
riseq_17.Insert((Int) i_19); e_set_15 = riseq_17; [‘set inds X’ halmaz generálásának vége
Int vdm_CopyPrTh_i;
{
Generic tmpe_22;
for
(int bb_21 = e_set_15.First(tmpe_22); bb_21 && tmpQuant_5; bb_21 = e_set_15.Next(tmpe_22)) {
Int elem_20 = tmpe_22;
succ_14 = true;
vdm_CopyPrTh_i = elem_20;
if (succ_14) {
if (((Bool) ((Generic) vdm_CopyPrTh_Y[vdm_CopyPrTh_i.GetValue()] ==
vdm_CopyPrTh_f((Generic) vdm_CopyPrTh_X[vdm_CopyPrTh_i.GetValue()]))).GetValue()) {}
else
tmpQuant_5 = false; }
}
}
}
varRes_4 = (Bool) tmpQuant_5;
return varRes_4;
}
//
// THIS FILE IS AUTOMATICALLY GENERATED!!
//
// Generated by the VDM-SLtoC++ Code Generator
//
// Supported compiler: g++ version 2.7.2
//
#ifndef _CopyPrTh_h
#define _CopyPrTh_h
#include <math.h>
#include "metaiv.h"
#include "cg.h"
#include "cg_aux.h"
void init_CopyPrTh();
Sequence vdm_CopyPrTh_copy(Sequence);
Bool vdm_CopyPrTh_post_copy(Sequence, Sequence);
#endif
3. kísérlet: Programozási tételek definiálása VDM modulként. Az eldöntés tétele
(DecisionPrTh)…
module DecisionPrTh
parameters
types
elem
functions
t: elem -> bool
exports
all
definitions
functions
decision(X: seq of elem) ex: bool
post ex = exists i in set inds X & t(X(i));
end DecisionPrTh
4. kísérlet: Programozási tételek definiálása VDM modulként. A kiválasztás
tétele (SelectPrTh)…
module SelectPrTh
parameters
types
elem
functions
t: elem -> bool
exports
all
definitions
functions
select(X: seq of elem) which: nat
pre exists i in set inds X & t(X(i))
post which in set inds X and t(X(which));
end SelectPrTh
5. kísérlet: Programozási tételek definiálása VDM modulként. A keresés tétele
(SearchPrTh)…
module SearchPrTh
parameters
types
elem
functions
t: elem -> bool
exports
all
definitions
functions
search(X: seq of elem) ret: bool * nat
post let ret=mk_(ex,wh) in
ex => wh in set inds X and t(X(wh));
end SearchPrTh
6. kísérlet: Adattípusok definiálása VDM modulban. A multi-halmaz (MultiSet)…
Az eredetileg VDM-SL-ben íródott specifikációt ISO 646 szerintire kellett átírni a különleges jelek miatt. Az IFAD-VDM szoftver használata során derültek ki a következő meglepő eltérések (a szabványtól), amelyeket javítani kellett:
1) azonosítók beli '-' '_'-re;
2) az alábbi sor
diff_bag(m_1,m_2) == {e |-> num-bag(e,m_1)-
num_bag(e,m_1) | (e in set dom m_1) and
(num_bag(e,m_1)>num_bag(e,m_2))}
helyett:
diff_bag(m_1,m_2) == {e |-> num-bag(e,m_1)-
num_bag(e,m_1) | ((e in set dom m_1) and
(num_bag(e,m_1)>num_bag(e,m_2))):int}
module Multiset
parameters
types elem
functions
empty_bag: () -> bag;
num_bag: elem * bag -> nat;
plus_bag: elem * bag -> bag;
mems_bag: bag -> set of elem;
merge_bag,
diff_bag: bag * bag -> bag
definitions
types bag = map elem to nat1
functions
empty_bag: () -> bag
empty_bag() == {};
num_bag: elem * bag -> nat
num_bag(e,m) == if e in set dom m then m(e) else 0;
plus_bag: elem * bag -> bag
plus_bag(e,m) == m ++ {e |-> num_bag(e,m)+1};
mems_bag: bag -> set of elem
mems_bag(m) == dom m;
merge_bag: bag * bag -> bag
merge_bag(m_1,m_2) == {e |-> num_bag(e,m_1)+
num_bag(e,m_2) | e in set dom m_1 union dom m_2};
diff_bag: bag * bag -> bag
diff_bag(m_1,m_2) == {e |-> num_bag(e,m_1)-
num_bag(e,m_1) | ((e in set dom m_1) and
(num_bag(e,m_1)>num_bag(e,m_2))):int}
end Multiset
7. kísérlet: Adattípusok definiálása VDM modulban. A prioritási sor (P_queue)…
További meglepő eltérések az ISO 646-hoz képest:
1) '&' helyett '.';
2) 'all' helyett 'forall'
module P_queue
parameters
types Entry
functions
priority: Entry -> nat
exports
operations
ENTER: Entry ==> ();
EXTRACT: () ==> Entry | QUEUE_EMPTY
instantiations
Entries as Multiset(elem -> Entry)
types bag
functions
empty_bag: () -> bag;
num_bag: elem * bag -> nat;
plus_bag: elem * bag -> bag;
mems_bag: bag -> set of elem;
merge_bag,
diff_bag: bag * bag -> bag
definitions
state P_queue of
QUEUE: Entries'bag
init mk_P_queue(q) == q=Entries'empty_bag
end
operations
ENTER(e:Entry)
ext wr QUEUE
post QUEUE=Entries'plus_bag(q,QUEUE~);
EXTRACT() e: Entry | QUEUE_EMPTY
ext wr QUEUE
post if QUEUE=Entries'plus_bag then
e=QUEUE_EMPTY and QUEUE=QUEUE~
else
(e in set Entries'mems_bag(q_QUEUE)) and
(forall e' in set Entries'mems_bag(q_QUEUE) .
priority(e)>=priority(e') ) and
(QUEUE=Entries'diff_bag(q,QUEUE~))
end P_queue
§ IFAD VDM-SL Toolbox, amelynek egy korlátozott oktatási változata (Toolbox Lite) megtalálható J. Fitzgerald és P. G. Larsen „Modelling systems” c. könyvében.