Testing is an essential activity of software development, and despite the vast use of testing by the industry, little formal reasoning can be found in the scientific literature of the field. The project presents an extensively formal approach to glass box testing from the underlying language to the graph model of a program, its execution, and reasoning on preconditions for its paths. In this paper, programs are modelled as executable Control Flow Graphs and test requirements are paths of the graphs. We study a logic to infer the weakest precondition of a given path of the graph. Weakest preconditions let us reason on relations between test requirements, which in turn let us optimise the test requirements set. The model uses a minimal language with the integer data type and first-order logic. This language can be extended as defined in this work to suit the need of the reader. Several metatheorems are proved for any language extending the minimal language we provide, including soundness, completeness under the restrictions to obtain a weakest precondition formula, and undecidability.

Testning är en viktig aktivitet inom programvaruutveckling, och trots den omfattande användningen av testning inom industrin finns det få formella resonemang i den vetenskapliga litteraturen inom området. Projektet presenterar ett omfattande formellt tillvägagångssätt för glasbox-testning från det underliggande språket till grafmodellen för ett program, dess exekvering och resonemang om förutsättningar för dess vägar. I detta dokument modelleras program som exekverbara kontrollflödesgrafer och testkrav är banor i graferna. Vi studerar en logik för att härleda det svagaste förhandsvillkoret för en given väg i grafen. Svagaste förhandsvillkor låter oss resonera om relationer mellan testkrav, vilket i sin tur låter oss optimera testkravsuppsättningen. Modellen använder ett minimalt språk med datatypen heltal och första ordningens logik. Detta språk kan utökas enligt definitionen i detta arbete för att passa läsarens behov. Flera metateorem bevisas för alla språk som utvidgar det minimala språk vi tillhandahåller, inklusive sundhet, fullständighet under restriktionerna för att få en svagaste förhandsvillkorformel och oavgörbarhet.