University of Twente Student Theses
Predicate subtyping in VerCors
Dubbeling, T. (2024) Predicate subtyping in VerCors.
|
PDF
598kB |
| Abstract: | VerCors is a program verifier that can verify specifications for programs written in Java, C and PVL (VerCors own language with built-in support for VerCors specifications). These specifications are expressed through pre-conditions and post-conditions similar to JML (Java Modeling Language) annotations. Many Java and C programs use bounded integers, rather than mathematical integers. Meanwhile, VerCors can only reason about all integer-based types as mathematical integers. As such, VerCors cannot verify a program for the absence of integer overflows. Bounded integers can be seen as subtypes of integers. Predicate subtyping is a subtyping system in which a subtype gets constructed with a type and predicates on a term of said type. The terms of the constructed subtype are all terms of the original type for which all predicates hold. We have added predicate-based subtyping to VerCors as a more general solution to supporting bounded integers. In this thesis we will first show how to manually translate examples of the proposed subtyping system into the corresponding specification in a program. We will also establish supporting mathematical theory describing the relations between predicate subtypes. |
| Item Type: | Essay (Bachelor) |
| Faculty: | EEMCS: Electrical Engineering, Mathematics and Computer Science |
| Subject: | 54 computer science |
| Programme: | Computer Science BSc (56964) |
| Link to this item: | https://purl.utwente.nl/essays/100843 |
| Export this item as: | BibTeX EndNote HTML Citation Reference Manager |
Show download statistics for this publication
Show download statistics for this publicationRepository Staff Only: item control page