Rökfræði í hugbúnaðargerð

Dæmi í Alloy

Náið í Alloy pakkann áður en við byrjum. Dæmin miða við Alloy 4 en í kennslubók er rithátturinn miðaður við Alloy 3, frekari skjölun er að finna á heimasíðu Alloy.

FileSystem - einfalt

Í þessu dæmi ætlum við að búa til líkan af skráarkerfi. Við skilgreinum tvo hluti, skrár og möppur.

sig FSObject { 
    parent : lone Dir -- mengi með nákv. eitt stak
}

sig Dir extends FSObject {
    contents : set FSObject -- hvað er í möppunni
}	

sig File extends FSObject { } -- lýsir ekki skrám frekar

Til að skoða módel sem uppfylla þessa lýsingu er hægt að bæta við skipuninni

run {} for 3

Þá er búin til tóm umsögn (pred) og líkan með þrjá hluti af hverri gerð búið til. Ýtið á execute og skoðið öll möguleg módel.

Eins og sést er ekki mikill tengsl milli hlutanna og contents og parent eru út um allt. Til að laga þetta bætum við frumsendu/staðreynd (fact) við módelið, fact er eitthvað sem á alltaf að gilda, það er ekki hægt að slökkva á því.

fact { File + Dir = FSObject } -- FSObject er annað hvort FIle eða Dir
fact { 
    all d : Dir, o : d.contents | o.parent = d
}

Fyrri staðreyndin segir að það sé ekki til FSObject sem er ekki File eða Dir, + merkir sammengi í Alloy. Seinni staðreyndin er yrðing með algildisvirkja, takið eftir að við getum takmarkað o við eingöngu þá hluti sem eru í d.contents. Þessi staðreynd tengir saman contents og parent.

Ef við keyrum sömu skipun og áður og skoðum nokkur módel þá sjáum við að þetta lítur betur út, en engu að síður er hægt að hafa skrá sem hefur möppu sem parent en er ekki hluti af contents fyrir möppuna. Einnig er ekkert hér sem segir að skrárkerfið þurfi að vera í einu lagi.

Til að laga þetta bætum við rót í skrárkerfið. Þá skilgreinum við nýjan hlut Root

one sig Root extends Dir { } { -- one er Singleton pattern, 
    no parent -- einfaldari leið til að skrifa fact um Root
}

Root er af taginu Dir og hefur því contents vensl, no parent þýðir að parent venslin eru tóm fyrir Root og one á undan sig þýðir að aðeins er eitt tilvik til af Root. Þetta er einföld leið til að tryggja að rótin sé Singleton.

Síðan bætum við einni staðreynd við módelið

fact {
    FSObject in Root.*contents
}

sem segir að allar skrár og möppur eru hlutmengi í þeim skrám sem sjá má frá rót. Root.*contents er gegnvirk lokun venslanna contents. Þetta eru allir hlutir í

Í raun væri hægt að skrifa FSObject = Root.*contents en það er tvennt sem mælir gegn því. Fyrst er hægri hliðin í contents FSObject þannig að Root.*contents er bara FSObject hlutir. Í öðru lagi er einfaldara fyrir Alloy að vinna með in heldur en = fyrir mengi, formúlan sem er skrifuð verður örlítið minni. Engu að síður fæst sama niðurstaða ef við notum in og =.

Ein leið til að skoða módelin er að keyra run {} for 3 og fletta í gegnum módelin og sjá hvernig þau líta út. Önnur leið er að skrifa niður yrðingar sem eiga að gilda og spurja Alloy hvort það finni mótdæmi. Við gerum þetta með assert skipuninni. T.d. ef við viljum athuga hvort forsendurnar sanni að engir hringir séu í skráarkerfinu getum við skrifað

– engir hringir assert acyclic { – notum assert þegar við viljum að það sé ekki satt no d : Dir | d in d.^contents }

check acyclic for 5

Til að keyra þetta er hægt að stroka út run skipunina áðan.

Alloy forritið okkar er þá

sig FSObject { 
	parent : lone Dir -- mengi með nákv. eitt stak
}

sig Dir extends FSObject {
    contents : set FSObject -- hvað er í möppunni
}	

sig File extends FSObject { } -- lýsir ekki skrám frekar

one sig Root extends Dir { } { -- one er Singleton pattern, 
    no parent -- einfaldari leið til að skrifa fact um Root
}

fact { File + Dir = FSObject } -- FSObject er annað hvort FIle eða Dir

fact { 
    all d : Dir, o : d.contents | o.parent = d
}

fact {
    FSObject in Root.*contents
}

-- engir hringir
assert acyclic { -- notum assert þegar við viljum að það sé ekki satt
	no d : Dir | d in d.^contents 
}

check acyclic for 5

Þá fáum við skilaboðin No counterexample found... sem segir okkur að ekkert mótdæmi af stærð 5 er til.

Önnur yrðing sem við gætum sannreynt er hvort að allar möppur nema rótin hafi foreldri.

assert oneRoot { one d : Dir | no d.parent}
check oneRoot for 5

eða það mætti skrifa oneRoot sem { all d : (Dir - Root) | some d.parent} sem er jafngilt.

Ef við skoðum yrðingu sem er röng þá sjáum við hvernig við getum skoðað mótdæmi

assert Wrong {
   all obj,p : (FSObject - Root) | (obj.parent = p.parent)
}

check Wrong for 15

Við keyrslu fæst að til er mótdæmi, við getum ýtt á counterexample hlekkinn til að sjá það en það gæti verið fullstórt. Oft er betra að takmarka sig við minnsta mótdæmi, þá getum við keyrt check Wrong for 2 og séð að ekkert mótdæmi er til af stærð 2, check Wrong for 3 gefur hins vegar einfalt mótdæmi.