Contracts - Non-accessible pre-conditions

[Vicente J. Botet Escriba]

Hi,

we have a standard use case that  would need the use of private conditions. E.g. when we move an string lvalue, the single things that can be done with is to destroy and assign. To capture this condition we would need an internal state to reflect this condition.

If pre-conditions can not use non-accessible members, how this pre-condition can be expressed?

Let me suppose that we allow non-accessible members?
Without contracts, the implementation doesn't need to represent this internal state, if another function is used the behavior is undefined. This mean that when adding Contracts, the implementation should need to do something else when Contract validation is enabled, isn't it?
So the question is, wouldn't we need to standardize a compiler flag to state that the Contract validation is enabled/disabled?
Otherwise, how a program could be portable and as efficient as possible?

If we don't want that any non-accessible member can be used in a contract expression, don't we need at least a specific attribute to mean accessible only on contract expressions?

What am i missing? do we want to take care of this kind of pre-conditions?

Vicente

[Jonas Persson]

The caller of the function needs to be able to verify that it will not do an invalid call so it must be accessible. And a broken pre-condition is equally invalid regardless of wheter contracts are enabled or not, so the implementation needs to be the same in both cases.

  / Jonas

--

---
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/.

[David Rodríguez Ibeas]

Vicente raises an interesting point, are there any preconditions that might not be testable/accessible by the client? My experience is that I have hit this in some cases, with interfaces that require that 'stop' not be called unless 'start' has previously been called and that at the same time do not provide an accessor to whether the object had ever been started. But as Jonas mentions, the feeling when working with those APIs is that they were not well designed and imposed a burden on the user that has to track externally whether 'start' was called or not.

I don't have any example of a component that I would consider well designed and at the same time did not allow the client to determine before hand whether a given call would be a violation of the contract.

As a side note, is the precondition really that you cannot do anything other than assignment/destruction on a moved-from string? My believe was that "valid" meant that you can call any member function with no preconditions and then any member function for which preconditions are met. So this would be a perfectly valid program:

std::string src = "String that might or not fit SMO";
std::string dst = std::move(src);
if (!src.empty()) {
    std::cout << "First character after move: " << src[1] << '\n';
}

Which again falls within what Jonas mentioned: the caller is able to determine whether a call to 'operator[]' will be within contract by calling other member functions that have wide contracts.  The precondition on 'operator[]' can be expressed in terms of the publicly available 'src.size()'.

Whether you believe that it is sane or not to try to reuse a string after being moved this way is a different question, but the contracts for the different members should not depend on what happened in the past, but the current state of the object. If the string after being moved is empty you cannot access the 1st element, how the string became empty is not part of the contract. If the string is non-empty, it does not matter whether move was called before, it is not empty and the call is within contract.  

If you want to add additional diagnostics specifically for this (using an object that has been moved-from), you could use an extension similar to checked iterators for containers. In that extension, the test could either be internal or the additional state would have to be accessible for the caller to verify.

    David

[Andrzej Krzemieński]

First, there are some "prerequisites" that we put on the input values that are impossible to verify:

void call_f(R* r)
// requires: r points to a valid object of type R (or related) whose life-time is in progress
{
  r->f();
}

There is no practical way to verify that the memory pointed to by r is a valid object (as opposed to raw memory). So, the preconditions as language feature can only express a subset of requirements. Regarding your example with strings, the statement that you can only destroy or assign to a moved-from object is incorrect. I recall that during the development of the C++11 standard it was often repeated that you can only perform these two operations, but the final outcome is that the moved-from object is in a "valid but unspecified state" (17.6.5.15 [lib.types.movedfrom]). According to this interpretation: http://stackoverflow.com/questions/7027523/what-can-i-do-with-a-moved-from-object, this means that you can invoke any member function on a moved-from object as long as it has "wide contract": on strings this would be size(), empty(), at().

So, I would say that the example with a moved-from string is not a good motivation for allowing private members in specifying a precondition. But to address your question, I believe that since the content of the precondition is part of the component's interface, it is required not to use private components. This implies that sometimes we would have to promote some part of the implementation public only for the sake of being able to express the precondition (I have encountered some cases like that) or accept that some requirements cannot be expressed with a precondition. This is needed because sometimes the programmer needs to "manually" check if his input satisfies the precondition of the function he is about to call, and this is checked by evaluating the precondition: in this case, the precondition needs to be accessible.

Regards,
&rzej

[Vicente J. Botet Escriba]

Le 24/04/15 09:13, Jonas Persson a écrit :

> The caller of the function needs to be able to verify that it will not
> do an invalid call so it must be accessible.

The user can know if the precondition is satisfied other than using a
public function. The context gives also some valid information.

> And a broken pre-condition is equally invalid regardless of wheter
> contracts are enabled or not, so the implementation needs to be the
> same in both cases.
>
>

You are right. Changing the implementation in order to be able to check
a contact seems not natural.

Vicente

[Vicente J. Botet Escriba]

Le 24/04/15 10:20, David Rodríguez Ibeas a écrit :

> Vicente raises an interesting point, are there any preconditions that
> might not be testable/accessible by the client? My experience is that
> I have hit this in some cases, with interfaces that require that
> 'stop' not be called unless 'start' has previously been called and
> that at the same time do not provide an accessor to whether the object
> had ever been started. But as Jonas mentions, the feeling when working
> with those APIs is that they were not well designed and imposed a
> burden on the user that has to track externally whether 'start' was
> called or not.
>
> I don't have any example of a component that I would consider well
> designed and at the same time did not allow the client to determine
> before hand whether a given call would be a violation of the contract.

The standard contains a contextual contract. tsd::mutex::unlock must be
called by the same thread that locked it.

>
> As a side note, is the precondition really that you cannot do anything
> other than assignment/destruction on a moved-from string?

Yes.

> My believe was that "valid" meant that you can call any member
> function with no preconditions and then any member function for which
> preconditions are met. So this would be a perfectly valid program:
>
> std::string src = "String that might or not fit SMO";
> std::string dst = std::move(src);
> if (!src.empty()) {
> std::cout << "First character after move: " << src[1] << '\n';
> }
>
> Which again falls within what Jonas mentioned: the caller is able to
> determine whether a call to 'operator[]' will be within contract by
> calling other member functions that have wide contracts. The
> precondition on 'operator[]' can be expressed in terms of the publicly
> available 'src.size()'.
>

There is a long thread about this (see [std-discussion] side effects of
moving standard types)

> Whether you believe that it is sane or not to try to reuse a string
> after being moved this way is a different question, but the contracts
> for the different members should not depend on what happened in the
> past, but the current state of the object. If the string after being
> moved is empty you cannot access the 1st element, how the string
> became empty is not part of the contract. If the string is non-empty,
> it does not matter whether move was called before, it is not empty and
> the call is within contract.
>
> If you want to add additional diagnostics specifically for this (using
> an object that has been moved-from), you could use an extension
> similar to checked iterators for containers. In that extension, the
> test could either be internal or the additional state would have to be
> accessible for the caller to verify.

The particular case of the move operation could be managed by compile
time pre/post conditions as suggested by Andrzej. Andzej suggest the use
of properties as e.g.

template <typename T>
property bool is_partially_formed (T const&);


T&& move(T& t) [[post: is_partially_formed(t) ]]
X& X::X(const& X x) [[pre: ! is_partially_formed(x) post: !
is_partially_formed(*this) ]]

Any other operation than destruction and assignment

R X::f() [[pre: ! is_partially_formed(*this) ]]

X x; // doesn't have property is_partially_formed yet.
X y = std::move(x); // x has property is_partially_formed now.
x = makeX(); // x doesn't have property is_partially_formed anymore

Vicente