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

Tehtävä 1

1. Mitä invariantteja luentomonisteessa esitettyyn VDM-kirjastospesifikaatioon voisi lisätä?
(Käy läpi kaikki tilamuuttujat ja mieti, onko kaikki niitä koskevat rajoitteet ilmaistu invarianteissa, erit. books)

2. Tarkastele uusien invarienttien suhteen sitä,

1. ovatko ne ristiriidassa aikaisempien kanssa?
2. pysyvätkö ne voimassa järjestelmässä määritellyille operaatioille?