Pensumboken er
Peter C. ?lveczky: Designing Reliable Distributed Systems: A Formal Methods Approach Based on Executable Modeling in Maude. Springer 2018 (st?r muligens 2017 i boken). Boken skal v?re tilgjengelig hvis man sitter p? UiO's nettverk. Boken er til salgs p? UiOs bokhandel "Akademika" (underetasjen).
Som hovedregel er boken, alle forelesninger med foiler, ukeoppgaver med l?sningsforslag og obligatoriske oppgaver pensum. Fra kompendiet utg?r fotnoter og de markerte "ikke-pensum" delene (avsnittene merket med "stjerne"). Kapitlene 7 (og muligens 17, vi f?r se hvor langt vi kommer) er ikke pensum i IN-2100. Beviset for at terminering er uavgj?rbart (med Turingmaskiner og greier) og den elegante teorien rundt forenklingsordninger er dessverre ikke pensum. Dvs i kapittel 4.1 utg?r alt unntatt stoffet til og med Theorem 4.1 (beviset er ikke pensum). Videre utg?r kapittel 4.4 t.o.m. side 78, og 4.4.3 (dvs 4.4.1 og 4.4.2 er pensum, men ikke resten av 4.4).
I tillegg er artikkelen "How Amazon Web Services Uses Formal Methods" pensum.
St?ttelitteratur
Maude hjemmeside for manual, download, etc.
Filen prelude.maude leses inn automatisk av Maude og inneholder blant annet definisjonen av de innebygde modulene. Nyttig!
Maude for Windows
Emnet benytter spr?ket/systemet Maude. Maude kan lastes opp enkelt for Linux og MacOS fra http://maude.cs.illinois.edu. Det enkleste og beste for Windows-brukere har v?rt ? laste ned Ubuntu eller lignende, og kj?re Maude der. Maude for Windows har dermed ikke v?rt problematisk tidligere. Merk at vi ikke skal bruke CVC-4 eller noen annen SMT solver i kurset, s? man trenger ikke ? laste opp CVC-4 (eller Yices).
Husk ogs? at Ifi's linux-maskiner alle har installert Maude: bare ? gi kommandoen maude.