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. 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).
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. It is also for sale at the university bookstore "Akademika".
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 possibly 17 ; we'll see how far we get) are not part of the curriculum of IN-2100. 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.
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.