DropShadow: Instrumenting Go with Contracts and Automatic Property-Based Test Generation of Hyperproperties
Authors
Vesteraa, Kasper ; Brandhøj, Andreas Kjeldgaard ; Dieu, Dat Tommy Thanh
Term
4. term
Education
Publication year
2024
Pages
60
Abstract
This thesis explores and evaluates DropShadow, a testing framework for the Go programming language that combines contract-driven testing with property-based testing to automatically generate and run tests. Contracts are precise statements of what a function should do, written directly into the source code. Based on these contracts, the tool automatically creates tests that check both trace properties (what happens in a single execution) and hyperproperties (how multiple executions relate). The latter are handled using sequential self-composition, a technique that turns cross-run comparisons into a single combined run. The aim is to make property-based testing easier to use, reduce the manual work of writing tests, and provide broader automated checks of whether programs behave as specified. Integrating contracts in this way means the tool checks not only individual functions against their specifications, but also the functions that call them or are called by them, providing a cascading assurance of correctness throughout the program. Our evaluation indicates potential practical use in different settings and with various language constructs, while helping to mitigate contractual explosion, where the number of contracts and checks could otherwise grow uncontrollably.
Denne afhandling undersøger og evaluerer DropShadow, et testframework til programmeringssproget Go, der kombinerer kontraktdrevet test med egenskabsbaserede tests for automatisk at generere og køre tests. Kontrakter er præcise beskrivelser af, hvad en funktion skal gøre, og de skrives direkte i kildekoden. På den baggrund kan værktøjet automatisk skabe tests, der kontrollerer både egenskaber for én enkelt kørsel (trace properties) og egenskaber, der vedrører forholdet mellem flere kørsler (hyperproperties). De sidstnævnte håndteres med en teknik kaldet sekventiel selvkomposition, som omsætter sammenligninger på tværs af kørsler til én sammensat kørsel. Målet er at gøre egenskabsbaseret test mere tilgængelig, mindske det manuelle arbejde med at skrive tests og give bredere automatiske kontroller af, om programmet opfører sig som specificeret. Integration af kontrakterne betyder desuden, at ikke kun den enkelte funktion tjekkes mod sin specifikation, men også funktioner, der kalder den eller bliver kaldt af den, hvilket giver en kaskaderende sikkerhed for korrekthed gennem hele programmet. Vores evaluering peger på praktisk anvendelighed i forskellige sammenhænge og med forskellige sprogkonstruktioner, samtidig med at værktøjet hjælper med at begrænse kontrakt-eksplosion, hvor antallet af kontrakter og checks kan vokse uhensigtsmæssigt.
[This apstract has been rewritten with the help of AI based on the project's original abstract]
Keywords