Skip to content

Latest commit

 

History

History
109 lines (90 loc) · 3.05 KB

paper.md

File metadata and controls

109 lines (90 loc) · 3.05 KB
Raw
title document date audience author toc toc-depth
Class Invariants
TBD
2023-03-28
SG21
name email
Nick DeMarco
name email
Sean Parent
name email
David Sankel
true
4

\pagebreak

Revision History

  • R0 --- TODO

Executive Summary

We propose semantics for class invariants in C++, independent of a particular syntax. Additionally, we identify a set of standard library functions which are necessary to test class invariants in situations where implicit checks are impossible for a compiler to generate. Finally, we provide illustrative examples with a syntax inspired by [@P2461].

Semantic Principles

TODO: Preamble

  1. Invariants are checked as if they were postconditions of public constructors and non-const member functions.
  2. Invariants only have access to a const *this.
  3. Invariants have private access.

Motivation

  1. Conceptually, a class invariant is a property which holds whenever the state of a class instance is observed by code outside of that class's definition. (TODO: How do we handle public member access? That's observable too, and we don't have a model for enforcing invariants after, say, mystruct.field = -1)

  2. Invariants are simply expressions of constraints, and therefore have no need to modify the class instances they constrain. Outright modificiations of objects during an invariant test are unidiomatic at best.

  3. Clearly, invariants must be able to express constraints on the private state of class instances. We cannot imagine a useful implementation of invariants that lacks this property.

Example

class type {
  int _x{0};
  int _y{0};

invariant { 0 <= _x }
invariant { _x <= _y }
};

Acknowledgements

TODO

\pagebreak

references: