T. Kärkkäinen
Kurssi: Formaalit menetelmät 2002
Harjoitus 5: Ag B212.1 14-16

BlockHandlerin lisä- ja jatkokäsittelyä!

Tehtävä 1

1. Lisää luentomonisteessa esitetyn BlockHandlerin alkuperäiseen rakenteeseen vaatimus siitä, että lohkojonon jokainen alkio on epätyhjä lohkojoukko.
   Keksitkö järjestelmälle lisää sitä sitovia invariantteja?
   
2. Miten varmistut lisäinvarianttien ja koko syntyvän invarianttijoukon ``järkevyydestä'' (V&V)?
3. Määritä kohdan 1 perusteella täydentyneelle järjestelmälle operaatio

   DoAddBlocks: Lisätään annettu lohkojoukko lohkojonon perään.

Tehtävä 2

Määritä BlockHandlerin yksinkertaistetulle ja tehtävän 1 invarianteilla täydennetylle rakenteelle operaatio

DoFreeBlocks: Mitkä muistilohkot ovat vapaina?

Tehtävä 3

Määritä luentomonisteen UserBlockHandlerille operaatio

DoBlocksofUserinQue: Mitkä annetulle käyttäjälle varatut muistilohkot ovat lohkojonossa?