Tool Support For Axiomatic Programming
Carla Villoria · OakTrust (Texas A&M University Libraries) · 2010
Many problems arising from spectacular error messages involving C++ templates are related to the fact that assumptions made by the C++ standard algorithms are stated in informal comments, not in code that is checked by the compiler. Some of those properties are syntactic, meaning that the compiler can do syntax and type checking and reject erroneous constructs. Others are semantics, e.g. that a type is regular. Such assumptions can be checked only if programmers have ways to express those assumptions in code. My project proposes to augment a subset of C++ with concepts and axioms that would let programmers express semantics requirements.