Predicate Subtypes in VerCors

TL;DR

This paper introduces predicate subtypes in VerCors, enabling precise range constraints and overflow checking, with automatic specification generation and support for combining multiple subtypes.

Contribution

It extends VerCors with predicate subtypes, supporting automatic specification, subtype combination, and a strict mode for overflow detection.

Findings

Prototype implementation integrated into VerCors.

Supports combining multiple subtypes for a single variable.

Enables overflow checking with a strict mode.

Abstract

Predicate subtypes provide an attractive mechanism to specify range constraints on variable declarations. This paper discusses how we add support for predicate subtypes to the VerCors program verifier. Our approach automatically generates appropriate specifications from predicate subtype declarations. It provides support to easily combine multiple subtypes for a single variable declaration. Moreover, in order to use predicate subtypes for overflow checking, a special strict mode is introduced, where every subexpression also has to stay within the declared subtype. A prototype implementation is integrated into the VerCors verifier.