Tölvumál - 01.06.1994, Síða 29

Júní 1994
__PayCompanyProfits_________________________________________
c? : Company
vessels‘1 : Company >—> P Vessel
í? : Month
yl : Year
FixedCost? : Vessel —> Kronur
TotalQuotaTrades‘1 : Vessel x lear —»■ Kronur
TotalOperatingCostl : Vessel X Year —> Kronur
TotalLandings? : Vessel X Year —> Kronur
TotalSharel : Vessel X Year —> Kronur
AProfits : Company X Year —> Kronur
tl mod 12 = 0
vesselsl c? 0
Profits' = Profits © {(c?, y?)
Evvevessels? e?(( TotalLandingsl v yl) - (TotalSharel v </?)-
(TotalOperatingCost? u </?) — (FixedCost? v </?)+
( TotalQuotaTrades? v </?))}
Mynd 3
abstract, en ritin ein og sér eru
ekki nógu tæmandi, því þau lýsa
ekki gagnaskilyrðum eða fyrir-
og eftirskilyrðum einstakra að-
gerða. í fyrstu notuðum við texta
til að lýsa þessum skilyrðum en
komumst að því seinna að form-
legar aðferðir henta betur til þessa.
Formleg skilgreining
Formleg aðferð er það kallað
þegar stærðfræði er notuð til að
lýsa hugbúnaði.Þetta er oft á
tíðum ekki flókin stærðfræði,
mest mengja- og rökfræði.
Nú halda margir að formlegar
aðferðir snúist einungis um það
að sanna að forrit séu rétt. Reyndar
er það stundum gert en réttara er
að segja að formlegar aðferðir
felist í því að skrifa formlegar
skilgreiningar á hugbúnaði og
stundum reynum við svo að sanna
eitthvað um eiginleika þessara
skilgreininga.
Hægt er að nota formlegar
aðferðir í mismunandi mæli, sem
er stundum skipt niður í nokkur
stig3:
Stig 1 - Einhver stærðfræði notuð
t.d. a og b,eðax er ímengi M.
Stig 2 - Formleg skilgreiningar-
mál með einhverjum hjálpar-
tækjum.
Stig 3 - Formleg skilgreiningar-
mál með hjálpartækjum til að
sanna skilgreiningar.
Stig tvö hefur verið vinsælla í
Evrópu, en stig þrjú í Bandaríkjun-
um.
I fiskveiðistjómunarlíkaninu
höfum við verið að prófa okkur
áfram með að nota formlega skil-
greiningu á stigi tvö. Til eru þó
nokkur formleg skilgreiningar-
mál, sum þeirra keyrsluhæf, en
við höfum notað Z4 málið. Það er
þróað í Englandi og til eru nokkrar
hlutbundnar viðbætur við það.
Verið er að staðla Z málið.
A mynd 3 er dæmi um skil-
greiningu í Z. Fyrir ofan strik eru
skilgreiningar en fyrir neðan strik
eru fyrir- og eftirskilyrði. Dæmið
sýnir hvernig fyrirtæki fær borg-
aðan hagnað af veiðiferðum báta
sinna á ári. Breytumar sem merkt-
ar eru með spumingarmerki eru
inntak, en breytumar sem auð-
kenndar eru með delta merkinu
eru bæði inntak og úttak, þ.e. þær
breytast í fallinu. Sumar skil-
greininganna eru föll, eins og t.d
vessels? erfallsemhefurfyrirtæki
sem inntak og úttakið er mengi
báta fyrirtækisins. Annað dæmi
er TotalOperatingCost? sem er
fall sem gefur heildar breytilegan
kostnað báts á tilteknu ári.
Með formlegu skilgreiningar-
máli er síður hætt á villum þó svo
að það eitt sér sé engin trygging
fyrir því að þetta verði allt rétt.
Kostirnir við að nota formlegt
skilgreiningarmál eru þeir að lýs-
ingin verður nákvæmari, en gefur
samt mikið frelsi til að lýsa hlutun-
um á fljótlegan hátt, þ.e. án þess
að þurfa að hugsa um útfærslu.
Nýverið hefur verið ákveðin
þróun í þá átt að nota formlegar
aðferðir í fyrri hluta þróunarferils-
ins, þ.e. meira í þarfagreiningu og
minna í sönnun forrita. Það má
rökstyðja notkun bæði í byrjun
og í lok hugbúnaðargerðar en oft
reynist dýrt að gera villur í þarfa-
greiningu eða hönnun og þess
vegna er lögð meiri áhersla á að
nota formlega skilgreiningu í
þeim þáttum.
29 - Tölvumál