Målet med den här C-uppsatsen är att få ett formellt bevis för att försvagning av kontrakt definierar en subtyp av en specifik typ. Att ”försvagning av kontrakt definierar en subtyp”, är en hypotes uppställd av Software Engineering Research Group (SERG) vid Karlstads universitet. I tidigare arbeten har Barbara Liskov presenterat substitutionsprincipen som definierar begreppet subtyp. Substitutionsprincipen anger dock endast om en typ är en subtyp av en annan typ, inte tillvägagångssättet. Krishna Kishore Dhara presenterar en egen definition av en subtyp och med hjälp av en teknik för specifikationsarv är det möjligt att specificera under vilka förutsättningar en typ är en subtyp av en annan typ. Dhara har bevisat att om kraven för specifikationsarv är uppfyllda så är också kraven för en subtyp uppfyllda. Dharas definition baseras på Liskovs ursprungliga men Dharas teknik baseras på matematik och är en komplex metod att använda. Vid varje enskilt tillfälle måste det visas att kraven är uppfyllda för specifikationsarv. SERG:s angreppssätt att varje gång visa att ett kontrakt är svagare än ett annat är enklare men det leder som sagt till en hypotes. Uppsatsens mål är att visa att SERG:s försvagning av kontrakt uppfyller Dharas villkor för specifikationsarv och erhålla ett formellt samband. En annan viktig slutsats med uppsatsen är att SERG:s definition inte är tillräcklig. Detta följer av försöken att bevisa hypotesen. Uppsatsen innehåller därför ett extra avsnitt där det bevisas att SERG:s definition inte är tillräcklig inklusive en komplettering av definitionen.