contract programming: invariants or axioms?

[Andrzej Krzemieński]

Hi Everyone,
I wanted to share, and run through the community, one thought about contract programming features. Namely, that axioms (like those in concepts) are a superior alternative to invariants.

One of the goals of contract programming support in C++ would be to assist with static analysis. For instance, given the following pre-/post-conditions for std::optional

T& optional<T>::operator*()
precondition{ bool(*this) };

T& optional<T>::operator=(T&&)
postcondition{ bool(*this) };

Compiler should be able to deduce the following:

// warning: precondition likely not met

void apply(function<void(int)> f, optional<int> i)
{
  f(*i);
}

// safe (checked manually):
void apply1(function<void(int)> f, optional<int> i)
{
  if (i) { f(*i); }
}

// safe (postcondition matches the precondition):
void apply2(function<void(int)> f, optional<int> i)
{
  i = 0;
  f(*i);
}

// safe (preferable):
void apply3(function<void(int)> f, optional<int> i)
precondition{ bool(i) }
{
  f(*i);
}

// no warning, at your own risk:
void apply4(function<void(int)> f, optional<int> i)
{
  [[ satisfied(bool(i)) ]] f(*i);
}

// safe (but tricky):
void apply3(function<void(int)> f, optional<int> i)
{
  if (i == nullopt) { i = 0; }
  f(*i);
}

"Safe" is not a guarantee that the precondition would hold (what if value is changed asynchronously?) but still it allows a certain degree of comfort.

The last example is problematic: how should the compiler know that contextual conversion to bool and the comparison against nullopt are 'compatible'? This could be done with an invariant, but could as well be done with an axiom (as described in N2887). The latter appears a more universal choice.

for instance, if something is sorted, it is also partitioned:

template <ForwardIterator IT, BinaryPredicate<ValueType<IT>> PR>
axiom being_sorted(IT b, IT e, PR p, ValueType<IT> v)
{
  is_sorted(b, e, p) => is_partitioned(b, e, [](auto x){ return p(x, v); });
}

template <Integal I>
axiom being_sorted(I i)
{
  is_positive(i) => is_nonnegative(i);
}

This could be expressed as an invariant:

class Integral {
  invariant {
    !is_positive(*this) || is_nonnegative(*this);
  }
};

But it looks more like a hack and puts some restrictions on the order of definitions: should Integral be defined first or function is_positive? Also, an axiom may be stated on two different types. In that case, it is not clear in the body of whose type  type the corresponding invariant could should be put:

axiom (XVector v, XMatrix m)
{
  v * m <=> m * transposed(v);
}

You could arbitrarily pick one, but the relation applies to both classes.

It looks to me that axioms are a generalization (or a superset) or invariants. Perhaps they should be an integral part of contract programming. I wonder what others think.

Regards,
&rzej

[Jeffrey Yasskin]

Do you have any examples of static analysis tools that are helped in
practice by either declared invariants or declared axioms? I hear a
lot of claims from the contract programming crowd that invariants and
axioms should help static analysis, but I've heard very little from
the people actually writing such tools. I really want their experience
to drive whatever design C++ moves toward.

> --
>
> ---
> You received this message because you are subscribed to the Google Groups
> "ISO C++ Standard - Future Proposals" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to std-proposal...@isocpp.org.
> To post to this group, send email to std-pr...@isocpp.org.
> Visit this group at
> http://groups.google.com/a/isocpp.org/group/std-proposals/?hl=en.
>
>

[Tony V E]

Might be worthwhile to take a look at the Assertion Definition Language: http://adl.opengroup.org/

Tony

[Lawrence Crowl]

On 6/10/13, Andrzej Krzemieński <akrz...@gmail.com> wrote:
> It looks to me that axioms are a generalization (or a superset) or
> invariants. Perhaps they should be an integral part of contract
> programming. I wonder what others think.

You are probably right, but I wonder if generalizing that way is
going to exceed our experience. That is, do you think it possible
or reasonable to define the simpler form, get use experience, and
then extend?

--
Lawrence Crowl

[Lawrence Crowl]

On 6/10/13, Jeffrey Yasskin <jyas...@google.com> wrote:
> Do you have any examples of static analysis tools that are helped
> in practice by either declared invariants or declared axioms? I
> hear a lot of claims from the contract programming crowd that
> invariants and axioms should help static analysis, but I've heard
> very little from the people actually writing such tools. I really
> want their experience to drive whatever design C++ moves toward.

Sun's compiler had pragmas that looked alot like invariants. They
we pretty simple, like count < n or count % 4 == 0. The optimizer
used them to guide optimization and strip out unnecessary code.

The problem was that the syntax was not portable. Programmers do
not want to spend a lot of time on platform-specific annotations
if they can avoid it. So, it didn't get used much.

I don't know that we have much experience chaining the postcondition
from on call into the preconditions of another call, but having that
information would certainly let static analysis programs point out
when the code looks incomplete.

I think we are in a bit of a bind here. Without a standard syntax
for saying such things, no one will properly develop the tools.

--
Lawrence Crowl

[Jeffrey Yasskin]

People used 'override' when it was just Microsoft, and we're using
[[clang::fallthrough]] even though it's just clang. People in
companies that use Coverity or Klocwork are just as likely to be
willing to add annotations that would make those tools work better. If
those companies haven't come up with such annotations, that's a mark
against trying to invent something for them to use.

[Andrzej Krzemieński]

Standardizing something beyond experience -- yes, this would be likely a mistake. However, there are still two ways to proceed. Either standardize today today's experience with contract programming, or wait until community's experience grows and standardize it in the future.

My personal impression was that contract programming proposals offered too little. Putting aside the interaction with class hierarchies, we get: guaranteed (under certain configuration) automatic runtime checks, and optimizations based on the assumptions that contracts hold. (At lest this is my understanding of the proposals.)

What I find missing is static checking if contracts are satisfied. You cannot standardize automatic bug detection, but you can make sure that programmers have enough means to convey their intent to static analysers and such. Without such support contract programming features appear incomplete. At least in the sense that certain static transformations are performed, but it is not checked if they are safe.

I talked about axioms a lot. I guess I confused two things a particular feature with static analysis support in general.

Regards,
&rzej

[J. Daniel Garcia]

While it is true that we may not have enough experience in C++, there are other languages where we can find experience.

Ada 2012 could be a relevant reference in this area

--

J. Daniel

--
 
---
You received this message because you are subscribed to the Google Groups "ISO C++ Standard - Future Proposals" group.
To unsubscribe from this group and stop receiving emails from it, send an email to std-proposal...@isocpp.org.
To post to this group, send email to std-pr...@isocpp.org.

Visit this group at http://groups.google.com/a/isocpp.org/group/std-proposals/.
 
 

[Gabriel Dos Reis]

Andrzej Krzemieński <akrz...@gmail.com> writes:

[...]

| What I find missing is static checking if contracts are satisfied.

How do you propose to check that the second argument to std::find (that
satisfies the requirements of an input iterator) is reachable from the
first argument? (Preconditions of the std::find algorithm.)

-- Gaby

[Andrzej Krzemieński]

Do you mean, how static analyser can verify the correctness? It is not of course possible to verify it in every case.  I imagine the following definitions would be in place (I use some invented contract syntax):

  template <typename I>
  bool is_valid_range(I b, I e); // not defined: just a tag

  template <typename T>
  axiom vec_range(std::vector<T> v)
  {
    is_valid_range(v.begin(), v.end());
  }

  template<typename I, typename V> requires ...
  I find(I b, I e, V v)
  precondition{ is_valid_range(b, e); }
  postcondition(f) {
    is_valid_range(b, f);
    is_valid_range(f, e);
    // ... more
  }

Now, if someone writes code:

  std::vecotr<int> vi = {...};
  auto i = std::find(vi.begin(), vi.end(), 7);
  auto j = std::find(i, vi.end(), 7);

The first call to find can be verified by matching axiom vec_range with the precondition. The second call can be verified by matching find's postcondition. is_valid_range is something like a 'property' or a 'tag' that is usually not evaluated. Objects obtain this property and hold it as long as no mutable operation is called upon them.

It would still not work though, because end() is not const, even though it doesn't change validity of the property...

Regards,
&rzej

[Gabriel Dos Reis]

Andrzej Krzemieński <akrz...@gmail.com> writes:

| W dniu piątek, 14 czerwca 2013 11:21:14 UTC+2 użytkownik Gabriel Dos Reis
| napisał:
|
| Andrzej Krzemieński <akrz...@gmail.com> writes:
|
| [...]
|
| | What I find missing is static checking if contracts are satisfied.
|
| How do you propose to check that the second argument to std::find (that
| satisfies the requirements of an input iterator) is reachable from the
| first argument? (Preconditions of the std::find algorithm.)
|
|
| Do you mean, how static analyser can verify the correctness? It is not of
| course possible to verify it in every case. I imagine the following
| definitions would be in place (I use some invented contract syntax):
|
| template <typename I>
| bool is_valid_range(I b, I e); // not defined: just a tag
|
| template <typename T>
| axiom vec_range(std::vector<T> v)
| {
| is_valid_range(v.begin(), v.end());
| }
|
| template<typename I, typename V> requires ...
| I find(I b, I e, V v)
| precondition{ is_valid_range(b, e); }
| postcondition(f) {
| is_valid_range(b, f);
| is_valid_range(f, e);
| // ... more
| }

One property of input iterators is that once copied, the original can't
be used again. Also, I am not sure what the purpose of is_valid_range()
is; the comment says it isn't defined.

-- Gaby

[Lawrence Crowl]

On 6/14/13, Andrzej Krzemieński <akrz...@gmail.com> wrote:
> My personal impression was that contract programming proposals
> offered too little. Putting aside the interaction with class
> hierarchies, we get: guaranteed (under certain configuration)
> automatic runtime checks, and optimizations based on the
> assumptions that contracts hold. (At lest this is my understanding
> of the proposals.)
>
> What I find missing is static checking if contracts are
> satisfied. You cannot standardize automatic bug detection, but
> you can make sure that programmers have enough means to convey
> their intent to static analysers and such. Without such support
> contract programming features appear incomplete. At least in the
> sense that certain static transformations are performed, but it
> is not checked if they are safe.

I don't see why the ability to do static checking of contracts does
not fall out of pretty much any contract proposal. Consider

type* producer();
void consumer(type* arg) preconditon { arg != NULL };
....; consumer(producer()); ....

The compiler that the postcondition of the call to producer is
insufficient to satisfy the precondition of the call to the consumer.
A tool can can warn in this case.

On the other hand, in

type* producer() postcondition { result != NULL; };
void consumer(type* arg) preconditon { arg != NULL; };
....; consumer(producer()); ....

the postcondition easily satisfies the precondition. The compiler
can avoid generating the precondition check based on that
satisfiability.

Compilers are not going to be able to always prove that functions
preconditions are satisfied. Indeed, I expect some preconditions
would be hard to specify in code, and so would be out of reach of
any automation. So, I don't know what we could normatively say
about static checking of interfaces. We can provide the data,
and hope tool writers do good things with it.
I think they will because in the second case above,
a warning would encourage the programmer to either make
the postcondition more complete or add an explicit check.

I think analyses that complement the cases were the compiler
exploits undefined behavior would be particularly valuable.
For example, in

int load(int* p) { return *p; }

loading through a null pointer is undefined behavior, so a tool
could infer a missing precondition and warn the programmer that
the function precondition is incomplete.

int load(int* p) precondition { p != NULL; } { return *p; }

Adding that precondition means that calls to load are now amenable
to analysis.

--
Lawrence Crowl

[Lawrence Crowl]

On 6/14/13, Gabriel Dos Reis <g...@axiomatics.org> wrote:
> Andrzej Krzemieński <akrz...@gmail.com> writes:
> > 14 czerwca 2013 Gabriel Dos Reis:

We could probably check this with type state, but certainly the
earlier contract programming proposals do not have mechanisms
for that.

--
Lawrence Crowl

[Gabriel Dos Reis]

Lawrence Crowl <cr...@googlers.com> writes:

[...]

| I think analyses that complement the cases were the compiler
| exploits undefined behavior would be particularly valuable.

In the scope of C++, I think this is probably the most compeling case
for "programming by contract."

-- Gaby

[Gabriel Dos Reis]

and assuming we know how to model the concept of input iterators
adequately...

-- Gaby

[Andrzej Krzemieński]

Really? I used to think that it is operation *it++ that invalidates the copies of the input iterator, not the copying itself. Also, your example is tricky because it tests a couple of difficulties at the same time:

• A predicate that cannot be formed
• A predicate that has side effects when it is evaluated
• A predicate on two arguments that are created separately from one another
• A predicate on non-value semantic types (we use iterators as references to remote objects/memory)

so, let me only address the first bullet here, by using a simpler example:

T& optional<T>::operator*()
precondition{ is_initialized(*this) };

T& optional<T>::operator=(T&&)
postcondition{ is_initialized(*this) };

And imagine that for some reason is_initialized cannot be formed/define. This is_initialized would be used by static analyser not as a function, which can be evaluated, but as a "tag" or a "label". Objects at certain points in time acquire the label, keep it for certain time, and then, they can loose it as an effect of a mutable operation.

void fun( optional<T> & o )
{
  // property is_initialized(o) cannot be determined
  o = T{1};
  // is_initialized(o) holds, even though we do not know what it means
  *o; // precondition is met
  mutable_fun(o);
  // property is_initialized(o) cann no longer be determined to hold
}


Regards,
&rzej

[Andrzej Krzemieński]

True, if one function's postcondition is _exactly_ same as other function's precondition, then static analyser can exploit this in any contract programming framework. The situation is different when preconditions and postconditions cannot be matched exactly. For instance, one function ensures property is_positive(e) and another requires property is_nonnegative(e). The former implies the latter, but the analyser would not know it. Similarly, there could be more than one way of stating the same state. In case of pointer, it is bool(p) and p != nullptr. Because pointers are built into the language compilers/analysers can understand the "redundancy" in the interface, but in similar case of std::optional, automated tools will not know that bool(o) is equivalent to o != nullopt. My personal opinion is that this element would be really missing from a "toolset" for enhancing static analysis. And on the other hand a construct for expressing such relationships has already been devised. Whether this ability is essential or not for the first "pass" of contract programming enhancements is I guess very subjective.
 

Compilers are not going to be able to always prove that functions
preconditions are satisfied.  Indeed, I expect some preconditions
would be hard to specify in code, and so would be out of reach of
any automation.  So, I don't know what we could normatively say
about static checking of interfaces.  

The standard could define the violation of the contract as undefined behaviour. This opens the way for contract based optimizations and instrumentation. And this is already so for cases like vector<T>::operator[].
 

[Lawrence Crowl]

On 6/17/13, Andrzej Krzemieński <akrz...@gmail.com> wrote:
> 17 czerwca 2013 Lawrence Crowl napisał:

> instance, one function ensures property *is_positive(e)*
> and another requires property * is_nonnegative(e)*. The former

> implies the latter, but the analyser would not know it.

If is_positive(e) and is_nonnegative(e) are inline functions
implemented as e>0 and e>=0, then the compiler certainly can make the
proper inferences. In any case, the compiler can only manipulate
predicates that are within its algebraic domain, and so it would
be best if preconditions were written to a reasonable domain.

> Similarly, there could be more than one way of stating the

> same state. In case of pointer, it is *bool(p)* and *p !=
> nullptr*. Because pointers are built into the language

> compilers/analysers can understand the "redundancy" in the

> interface, but in similar case of *std::optional*, automated
> tools will not know that* bool(o) *is equivalent to* o != nullopt*.

But if the postcondition on bool(o) is result == (o!=nullopt),
then that interpretation is within reach. It will take work to
specify preconditions and postconditions in a manner that is both
useful to compilers and to programmers.

> My personal opinion is that this element would be really missing
> from a "toolset" for enhancing static analysis. And on the other
> hand a construct for expressing such relationships has already
> been devised. Whether this ability is essential or not for the
> first "pass" of contract programming enhancements is I guess
> very subjective.

I am not sure that we are all that far from what you suggest, at
least for a reasonable subset of the preconditions. Can you write
a paper describing what you want in detail?

> > Compilers are not going to be able to always prove that functions
> > preconditions are satisfied. Indeed, I expect some preconditions
> > would be hard to specify in code, and so would be out of reach
> > of any automation. So, I don't know what we could normatively
> > say about static checking of interfaces.
>
> The standard could define the violation of the contract as
> undefined behaviour. This opens the way for contract based
> optimizations and instrumentation. And this is already so for

> cases like * vector<T>::operator[]*.

The prior proposals did define violation as undefined behavior.

[Andrzej Krzemieński]

I describe some examples of what I mean in the following draft paper:
http://htmlpreview.github.io/?https://github.com/akrzemi1/contract/blob/master/contract.html

Regards,
&rzej