A deklarációk definiálhatnak eljárásokat (proc, vproc, func és sel) és típusosztályokat (formák), megadhatják az objektumok állapotát (var, const) és az azonosítókat az entitásokhoz köthetik.
Deklarációk hatásköre
A deklarációk hatásköre az Algolban használtakhoz hasonló. A normál Algol hatáskörben a változók abban a blokkban érvényesek, ahol deklarálták õket, illetve azokban a belsõ blokkokban, ahol nem definiálják felül õket.
Segéd deklarációk
Bármely deklarációt megelõzheti az aux szó. Az így definiált változókat
azonban csak állítások megfogalmazásánál lehet használni. A segéd
deklarációk modell szerepet töltenek be a specifikációban.
Például az alábbi deklarációban:
form DirectGraph(size :int) is
specs
...
aux func IsTree(g:DirectGraph):boolean
post {returns true iff g is true };
...
end DirectGraph;
Ahol az IsTree eljárást csak specifikációkban használhatjuk.Távoli deklarációk
Egy entitás (változó, eljárás, forma) deklarációja nem esik mindig egybe a definíciójával. Az Alphardban a következõ három ilyen eset lehetséges:
1. forward: Azt jelenti, hogy az utána említett entitás pontos definíciója késõbb helyezkedik el a programban. Ilyen deklarációra például egymásra hivatkozó típusok definiálásakor van szükség.
2. as specified: egy forma specifikációjánál szükség lehet olyan entitás definíciójára, aminek azonos a specifikációja. Például ha egy forma implementációja egy olyan (objektum) paramétert feltételez, melyet futásidõben reprezentálunk.
3. external(<system specs>): néhány entitás definíciója a programon kívül megadott, (más fájlokban, könyvtárakban). Ilyen esetekben kell ezt a definíciót használni. A <system specs> egy rendszerfüggõ megjegyzés, ami azt a helyet jelöli, ahol a pontos definíció adott.
Címkék
<label decl> ::= label <identifier list>
Például:
label L1, EXIT, Rethink
A címkéket is, mint minden más entitást, használat elõtt kell definiálni. A címke a deklaráció hatáskörében csak egyszer használható.
Objektum deklarációk
<var decl> ::= <aux> var {<obj decl group>{<init fin clause>}#}+
<const decl> ::= <aux> const {<obj decl group>{<init fin clause>}# |
<const assign>},+
<aux> ::= {aux}+
<obj decl group> ::= <identifier list>:<obj type>
<obj type> ::= <type description> | as specified
<init fin clause> ::= = <expression> | {init<stmt>}# {final<stmt>#}
<const assign> ::= <identifier list> = <expression>
Példák:
var a,b,c:int, g:real
aux const a:int=5
var INF:file(vector(mumble,1,unk)) init open(INF)
var q,x,r:as specified
var Q:queue(int) init new(Q) final destroy(Q)
const ADD=0, SUB=1, MUL=2
Objektum deklarációk forma vagy blokk belsejében lehetnek. A két eset
különbözõ. A formák esetében a leírást lásd a forma deklarációk fejezetben.A konstans és változó deklarációk abban különböznek, hogy a konstans változókat nem lehet módosítani (de az init és final utasítások rájuk is vonatkoznak).
A változók felsorolása esetén a sorrend nem számit, az inicializáló eljárások mindegyikükre lefutnak, és mindegyikükhöz azonos típusú, de külön objektum kötõdik.
Egy as specified-al jelzett deklaráció csak forma implementációjában fordulhat elõ, ekkor a típusa a forma specifikációjának megfelelõ lesz.
Típus deklarációk kiértékelése
A típus deklarációk szintaktikailag olyan entitások, amelyek objektum
deklarációban és formális paraméter specifikációban fordulhatnak elõ.
<type description> ::= <simple invocation> {({<formal qual>},+)}#
{<update set>}# | ?<identifier>{<update set>}#
<formal qual> ::= <expression> | ?<identifier>{<update set>}# |
{<identifier>:}#<typedescription> | unk
<update set> ::= < {<identifier> | <special identifier> },+ >
ahol az <update set>-ben megadott külsõ <> jelek a nyelv részei. Példák:
integer
vector(real,1,10)
stack(T:form<&:=>,22)
collection(unk)
queue(process,?length)
A T(E1,...,En)<P1,...Pm> típus kiértékelése az alábbiakat jelenti:
1. Ei-k egy nem definiált sorrendben kiértékelõdnek. A kiértékelések
eredménye objektumok, eljárások és típusok lehetnek. A következõ speciális
esetek megemlítendõk:
a) egy unk kiértékelése unk-t eredményez
b) ?azonosító kiértékelése egy implicit kötést feltételez, csak
aktuális-formális paramétermegfelelésnél engedélyezett.
2. T formális paramétereinek száma n kell legyen (n>=0). Az aktuális paraméterek meg kell feleljenek a formálisoknak.
3. T lesz a bázis típus, és Pi a módosító halmaz.
Az <update set> lesz a típus módosító halmaza. Az itt szereplõ azonosítók a bázis típusban deklarált eljárások lehetnek. Ha ?azonosítót használunk, akkor az azonosítót késõbb kell deklarálni. Ha nincs <update set> záradék megadva, akkor a típus teljes módosító halmaza érvényes lesz, ha <> -t adunk meg, akkor a módosító halmaz üres.
Formális paraméterek
Az Alphardban mind a formák, mind az eljárások paraméterezhetõk - ezek leírása
adja meg a formális paramétereket.
<formals> ::= ({<routine formal> | <binding><obj formal> |
<type formal>},+)
<routine formal> ::= <formal id list> proc <parms> |
<formal id list> {vproc | func | sel} <vparms>
<binding> ::= {copy | {alias}#{const | var}}#
<formal id list> ::= <identifier list>:
<obj formal> ::= <formal id list> <type description>
<type formal> ::= <formal id list> {form | pform }{<update set>}#
Példák:
(const x:T1, var q:?T2, copy r:vector(?T2,1,n))
(T:form, h:proc(x:real):int)
A formális paraméterek adják meg a lehetséges aktuális paraméterek specifikációját, és az elérés azonosítóját. Paraméterezhetünk eljárással, objektummal és típussal.
Egy objektum paraméter specifikációját megelõzi egy leíró rész, aminek elemei a copy, const, var és alias lehetnek. A var és const használatakor referencia jellegû kötések jönnek létre az aktuális paraméter objektumra. A const használatakor azonban a módosító halma üres lesz, tehát ezen paraméterek értékét nem változtathatjuk. A copy-val jelzett paraméterek esetén létrejön egy új, megfelelõ típusú objektum, és az aktuális paraméter értékét az &:= értékadással megkapja. Az alias jellemzõnek nincs szemantikai jelentése, egyszerûen azt jelenti, hogy egy referencia paraméter átlapolhat-e már meglévõ referenciákat (ha alias jelen van, akkor igen).
Eljárások deklarációja
<routine decl> ::= <vproc decl> | <proc decl> | <sel decl>
<vproc decl> ::= <aux> {inline}# {vproc | func} <routine id>
<v parms>
<pre post> <assumes> {<routine body>}#
<proc decl> ::= <aux> {inline}# proc <routine id> <parms>
<pre post> <assumes> {<routine body>}#
<sel decl> ::= <aux> {inline}# sel <routine id> <v parms>
<pre post> <assumes> {<routine body>}#
<routine id> ::= <identifier> | <special identifier>
<parms> ::= {<formals>}#
<v parms> ::= {<formals>}#:<type description>
<pre> ::= {pre <assertion>;}#
<pre post> ::= <pre> {post <assertion>;}#
<routine body> ::= is <stmt> | is as specified | is forward |
is external (<system specs>)
Példák:
vproc f(x:int):real
pre {abs(x)<maxintreal};
is float(x);
inline sel trial(var A:vector(?T,1,?n), i,j:int):T
is A[i*(i-1) div 2+j)
proc empty is as specified
Szelektorok (sel) objektumokat nevesítenek. Eljárások (proc) végrehajtása állapotváltozást eredményez, és nincs visszatérési értéke. Értékvisszaadó eljárások (vproc) állapotváltoztatást eredményezhetnek, és lehet visszatérési értékük is. Függvények (func) hasonlóak az értékvisszaadó eljárásokhoz, de ezek determinisztikusak kell legyenek (ha &=(A,B) akkor &=(F(A),F(B))), és nem változtathatják a paraméterek állapotát. Ez eljárástörzs utasítása ez utóbbi két deklaráció (vproc, func) esetén egy egyszerû utasítás, aminek típusa az eljárás visszatérési típusa.
Az inline jellemzõnek nincs szemantikai jelentése, a fordítónak jelez, hogy a kódról másolatot kell készíteni minden hívási helyen (makrók).
A pre és post után adhatjuk meg az eljárásba lépés elõfeltételét, és az utófeltételt. A post-ban a result azonosítóval hivatkozhatunk az eljárás által visszaadott értékre.
Az eljárások törzse forma specifikációkban hiányozhat csak. Forma implementációban lehet as specified-al jelzett. Az eljárás lehet forward-nak specifikált, ha a deklarálás késõbb következik (de még a blokkon belül). Lehet external, ha egy rendszerfüggõ eljárás, amit a <system specs> specifikál.
Az assumes tag (implicit vagy explicit) generic paramétereket deklarál.
Formák deklarálása
A formák típusosztályokat definiálnak. Minden bázistípushoz létezik egy
form definíció. A láthatósági viszonyok a szokásosak.
<form decl> ::= <aux> form <identifier> {<formals>}# <pre> <assumes>
is <form body>
<form body> ::= {<specs>}# {<impl>}# end {<identifier>}# | <abbrev body> |
forward | external (<system specs>)| as specified
<specs> ::= specs { <var decl> | <other form decls> };+
<impl> ::= impl { <shared> <var decl> | <other form decls> };+
<other form decls> ::= <routine decl> | <form decl> | <axiom> |
<shared> <const decl>
<shared> ::= shared#
<axiom> ::= invariant <assertion> | initially <assertion> |
axiom <assertion> | repmap <assertion> |
rule <identifier> <assertion>
Példa:
form F(T :form, x:int) is
specs
var m:int;
vproc p(f:F):T pre {m<x} post {m>x}; ...
impl
const x:as specified
var m:as specified
vproc p is F.m:=F.x+1; ...
end
A specifikációs rész (<specs>) alatt adhatjuk meg a forma metódusait és tulajdonságait. Ezeket azonban újra kell deklarálni, ha használni akarjuk az implementációs részben (<impl>). Forma törzsében definiált formális paraméterekre ugyanez igaz, bár ezeket az as specified kulcsszóval újradefiniálhatjuk az implementációs részen belül.
A shared kulcsszó után olyan objektumokat deklarálhatunk, amik az egész osztály részére elérhetõk (minden adott típusú objektum számára).
A specifikációban nem osztottnak definiált objektumok eljáráshívásnak minõsülnek. Például:
form T ...
specs ...
var P:Q
const A:R
egy rövidítése a
form T ...
specs ...
sel P(var t:T):Q
func A(t:T):R
specifikációnak.
Rövidítések formák létrehozására
A forma törzsek rövidítésére két szokásos konstrukciót vezettek be az
Alphardban, a rekord és felsorolási típust.
<abbrev body> ::= <record type> | <enumerated type>
<record type> ::= record ({<obj decl group>,+)
<enumerated type> ::= enumerated ( <identifier list> )
Példák:
record(re,im:real)
record(x,y:int, load:real, theta:radians)
enumerated( red,blue,green,purple,bardot )
A
form F(...) is record (D1,D2,...,Dk)
deklaráció ekvivalens az alábbi deklarációval:
form F(...) is
specs
var D1,...,Dk;
func cons(D1,...,Dk):F(...);
func &=(lhs,rhs:F):boolean;
func &:=(var lhs,rhs:F):F(...);
impl
var D1,...,Dk;
func cons is
value v:F(...)
of note hozzárendelés v komponenseihez eton fo
func &= is note komponensek összehasonlítása eton
vprox &:= is note rhs -nek értékül adni lhs-t eton
end F
deklarációval.
A
form C is enumerated (I1,I2,...,In)
deklaráció pedig ekvivalens az alábbi deklarációval:
form C is
specs
shared const I1,...,In:C; !diszjunkt konstansok
func &=...; !egyenlõségvizsgálat
func &:=...; !értékadás
func min...; !elsõ elem =I1
func max...; !utolsó elem = In
func succ...; !következõ elem
func pred...; !elõzõ elem
func card...; !számossága (n)
func decode...; !sorszáma (I3->3)
func code...; !sorszámhoz elem
func spell...; !elem stringgé alakítása
func unspell...; !string alakítása elemmé
generator gen...; !generálja az elemeket
end C
Generátorok
A generátorok speciális formák. For és first vezérlési
szerkezetben gyakran használt típusok esetén definiáljuk õket.
<form decl> ::= <aux> generator <identifier> {<formals>}# :
<type description> <pre> <assumes> is <form body>
Példa:
generator upto(lb,ub:int): int is
specs
pre {ub<=maxint-1 and lb>=minint}
aux var k:int=ub+1;
rule for
{premise l<=k<=u and I([l..k-1]) {ST(k)} I([l..k])
concl I([]) {for k from g:upto(l,u) do ST(k)
od} I([l..u])}
rule first
{...}
impl var k:as specified;
const lb,ub:as specified;
func &done is g.k>g.ub;
sel &value is g.k;
proc &start is g.k:=g.lb;
proc &next is g.k+:=1;
proc &finish is g.k:=g.ub+1;
endof upto
A ciklusok elemeinek generálásához szükség van az alábbi eljárások definiálására: &start, &next, &done, &value. Az &finish megadása nem kötelezõ. A generátorokat csak a fent megadott két ciklusban használhatjuk.