|
|
String Analysis for Code Contracts
Dort, Vlastimil ; Parízek, Pavel (advisor) ; Kofroň, Jan (referee)
Using contracts such as method preconditions, postconditions, and class invariants in code is an approach to preventing bugs in object-oriented programs. In the .NET Framework, this is possible due to the framework of Code Contracts, which includes Clousot, a tool for static program analysis based on abstract interpretation. Although string is a fundamental type in .NET programs, Clousot does not have a usable support for analysis of string values. In this thesis, we explore the specifics of string manipulation in the C# language and in the .NET Framework, and show how they can be covered by static analysis. Our approach is to use the methods of the String class and a subset of regular expressions to specify string properties in code, and to use abstract interpretation with non-relational abstract domains to reason about those properties. We chose a small number of already published abstract domains for strings, which vary in their complexity and ability to represent different properties. We adapted those domains to our setting, including definitions of abstract semantics for the supported string methods. We implemented the abstract domains in Clousot in a way that cooperates with numerical analysis and allows adding more string abstract domains in the future. Powered by TCPDF (www.tcpdf.org)
|
|
|
Verifying integrity constraints in C# using Code Contracts
Dort, Vlastimil ; Malý, Jakub (advisor) ; Ježek, Pavel (referee)
OCL serves as a language for specification of integrity constraints on UML models, Code Contract allow the integrity constraints to be expressed in programming languages targeting Microsoft .NET Framework. The goal of the thesis is to find and implement a translation of integrity constraints form the OCL language to C#, using Code Contracts. The features of Code Contracts and OCL are presented, then individual language constructs and standard library operations are compared with syntactic and semantic equivalents in C#. The chosen translation aims to match the semantics of OCL where possible. Code generation of C# sources is implemented in the eXolutio application, which provides a class diagram editor and an OCL parser. Powered by TCPDF (www.tcpdf.org)
|
guest ::
