C++ Logo


Advanced search

[wg14/wg21 liaison] the syntax for contract annotations in C++

From: Andrzej Krzemienski <akrzemi1_at_[hidden]>
Date: Mon, 20 Sep 2021 15:58:35 +0200
Hi SG22,
I hope I am using the right address for addressing the C/C++ liaison study

I was advised to consult the group about the syntax intended to be used for
contract annotations in C++ (preconditions, postconditions, and assertions).

Here is a link to the paper describing the proposed addition

The syntax is based on the contract proposal that targeted C++20. In short:

int select(int i, int j)
  [[pre: i >= 0]] // a function precondition
  [[pre: j >= 0]] // a function precondition
  [[post r: r >= 0]] // a function postcondition, r names the return value
  [[assert: _state >= 0]]; // block-scope assertion
  if (_state == 0) return i;
  else return j;

The syntax was chosen for the following reason:
* Some conceptual resemblance to attributes: removing them from a correct
(bug free) program does not affect the semantics
* Word `assert` can be used without conflicting with macro `assert()`.

I would like to know your opinion on how this is compatible with the plans
for C.

This is my first interaction with SG22, so I do not know how to proceed.
Should I give you a presentation of the feature in Zoom? Should we set up a
telecon to discuss, or is it fine to only exchange emails?

I would appreciate your guidance here.

I am also not subscribed to *liaison_at_[hidden]
<liaison_at_[hidden]>*,and in fact I do not know where to apply for
the subscription, so I would appreciate a direct answer to this email.

Andrzej KrzemieĊ„ski

Received on 2021-09-20 08:58:48