Pensumboken er
Peter C. ?lveczky: Designing Reliable Distributed Systems: A Formal Methods Approach Based on Executable Modeling in Maude. Springer 2018. Boken skal v?re tilgjengelig hvis man sitter p? UiO's nettverk.
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 17 er ikke pensum i INF3232. En endring i ?r er at beviset for at terminering er uavgj?rbart (med Turingmaskiner og greier) og den elegante teorien rundt forenklingsordninger ikke er 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).
English: The book
Peter C. ?lveczky: Designing Reliable Distributed Systems: A Formal Methods Approach Based on Executable Modeling in Maude. Springer 2018.
the main textbook for this course and is available from the above link if are using the University's network.
As a rule, this textbook, as well as all the lectures, supplementary material, exercises with their solutions, and mandatory assignments define the core curriculum of the course. However, the footnotes and those parts of the course book that are explicitly marked as non-core reading are not required reading. Chapters 7 and 17 are not part of the curriculum of INF3232. In addition, this year the proof of undecidability of termination and the very elegant theory of simplification orders is unfortunately not part of the curriculum. More precisely, in Section 4.1, only the first paragraph and the statement of Theorem 4.1 is part of the curriculum; the rest of 4.1 is not. Likewise, in Section 4.4, only Section 4.4.1 and 4.4.2 are part of the curriculum; i.e., 4.4.3 and the 4.4 until the end of page 78 are not.
INF4232
Pensum for INF4232 er som for INF3232, og i tillegg kommer Kapittel 17 og noe annet.
The curriculum for INF 4232 extends the one for INF 3232 with real-time and probabilistic systems (Chapter 17 of the book).
St?ttelitteratur/Supplementary resources
Maude hjemmeside for manual, download, etc.
Maude home page, for downloading, documentation, etc.
Filen prelude.maude leses inn automatisk av Maude og inneholder blant annet definisjonen av de innebygde modulene. Nyttig!
The file prelude.maude is read automatically by Maude and includes the definition of the built-in modules.
Maude-manualen anbefales for ? l?re mer om Maude og dens kommandoer.
The Maude manual is obviously a crucial resource.