To: J3                                                     J3/23-190
From: M. Haveraaen, generics
Subject: Properties for requirements
Date: 2023-June-13

Reference: 23-102r5i


1. Introduction
===============

Requirements define the interfaces for procedures so that template bodies
can be type-checked. A requirement often has a comment providing a semantic
intention, i.e., clarifying properties of the procedures being declared.
Template descriptions make claims based on such assumptions, and template
code is written assuming these properties.

For instance, a templated matrix library assumes that plus_t and times_t
behave like they do for numbers.

The suggestion is to make such assumptions explicit alongside the
requirement, thus benefiting both template authors and template users.



2. Prior art
============

The programming language Java uses normative property specifications in
library descriptions. For instance, the Java standard library demands that
any class which implements the interface Comparable be consistently
ordered. Any class implementing Comparable can be used in sorting
algorithms, be elements of binary search trees, etc.

C++ concepts also uses normative documentation in the standard library, and
compilers take advantage of these properties when optimising code.

Property specification have been used by testing tools, e.g., QuickCheck.
QuickCheck was developed for Haskell, but has seen success as a testing
tool for the Erlang programming language (telephone exchanges).

Ada 2012 introduced assertions to define properties. The Spark sublanguage
of Ada uses these properties to support verification of implementations.


The suggestion is to develop a way to express semantic properties so that
developers and processors can take advantage of them.

===END===