The field of contract theory is concerned with formal proofs of how smaller components may be composed into larger systems. This thesis shows how one framework for constructing such proofs may be used to prove properties of compositions where some components are specified using the TLA+ formalism. This is done by showing an equivalence between a TLA+ formula and an assume-guarantee contract and then carrying out a proof of compositionality utilizing the assume-guarantee contract. The components that are specified are part of a toy system previously specified in an earlier work, from where the bulk of the specifications used in the proof is taken. Furthermore, it is shown that any specification given in TLA+ is assertional, meaning that a composition with a component fulfilling such a specification preserves the component’s behavior.

Då ett komplext mjuk- eller hårdvarusystem ska specifieras är det praktiskt att skapa separata specifikationer för dess komponenter. Kontraktsteori är ett datalogiskt forskningsfält som undersöker hur man formellt kan visa att dessa delspecifikationer tillsammans ger en specifikation för hela systemet. Denna rapport visar hur ett sådant formellt bevissystem kan appliceras då ett system specificerats i termer av så kallade assume-guarantee-kontrakt samt med specifikationsspråket TLA+. Detta görs med utgångspunkt i ett exempelsystem, där vissa komponenter specificeras med TLA+. Vi visar att dessa TLA+-specifikationer kan visas vara ekvivalenta med ett assume-guarantee-kontrakt, vilket i sin tur kan visas vara komponerbart med andra specifikationer till ett system som uppfyller de givna kraven.