220 4964 <67dced99-d566-4082-94e1-2f831119e1cf@isocpp.org> article Path: news.gmane.org!not-for-mail From: =?UTF-8?Q?Andrzej_Krzemie=C5=84ski?= Newsgroups: gmane.comp.lang.c++.isocpp.proposals Subject: contract programming: invariants or axioms? Date: Mon, 10 Jun 2013 10:22:39 -0700 (PDT) Lines: 199 Approved: news@gmane.org Message-ID: <67dced99-d566-4082-94e1-2f831119e1cf@isocpp.org> Reply-To: std-proposals@isocpp.org NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: multipart/alternative; boundary="----=_Part_543_24950661.1370884959523" X-Trace: ger.gmane.org 1370884962 18401 80.91.229.3 (10 Jun 2013 17:22:42 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Mon, 10 Jun 2013 17:22:42 +0000 (UTC) To: std-proposals@isocpp.org Original-X-From: std-proposals+bncBDT2DGOJ34DBBYEW3CGQKGQEFPM4XBA@isocpp.org Mon Jun 10 19:22:44 2013 Return-path: Envelope-to: gclcip-std-proposals@m.gmane.org Original-Received: from mail-vb0-f72.google.com ([209.85.212.72]) by plane.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1Um5nm-0002lN-7q for gclcip-std-proposals@m.gmane.org; Mon, 10 Jun 2013 19:22:42 +0200 Original-Received: by mail-vb0-f72.google.com with SMTP id p12sf5812343vbe.3 for ; Mon, 10 Jun 2013 10:22:41 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=x-beenthere:date:from:to:message-id:subject:mime-version :x-original-sender:reply-to:precedence:mailing-list:list-id :x-google-group-id:list-post:list-help:list-archive:list-subscribe :list-unsubscribe:content-type; bh=n8z8Nr5dGsoiV5huH4BNE9GjHSyn9PdxGk4DZ5teYtg=; b=rcKvxy6MXM3GTNMgPTinoSl/mOA+syo3ow2qwSgLH+EbdmlnHn5u4tyXtMnU8lixRw vf2hff69s3D8t/XXH1XiAuyXm2Q9aT6OVHPVeY/b9GWfKrSx1W76nywVuweeKdybeQMf gTiQQAk60VMqkouzaBAW8GNyg1phg07TxjvNIRN7I9uPa1khOX/nRn199ZqvOcOB2xBe G08TH08m/8o+iWleDLLLP9sbvl7MO4LTGHN5HvRuHLgfDu2WbVDEo1cF6AIdFTje4XyG YytRy3JuONSi+yfsEHeTFRTcTXgbW/px5Ho6ccsbFO+ofgybmUrWwCVwxvNEb/32iLd/ om2Q== X-Received: by 10.224.42.141 with SMTP id s13mr8856871qae.3.1370884961317; Mon, 10 Jun 2013 10:22:41 -0700 (PDT) X-BeenThere: std-proposals@isocpp.org Original-Received: by 10.49.83.102 with SMTP id p6ls384767qey.63.gmail; Mon, 10 Jun 2013 10:22:40 -0700 (PDT) X-Received: by 10.49.62.168 with SMTP id z8mr496887qer.11.1370884959962; Mon, 10 Jun 2013 10:22:39 -0700 (PDT) X-Original-Sender: akrzemi1@gmail.com Precedence: list Mailing-list: list std-proposals@isocpp.org; contact std-proposals+owners@isocpp.org List-ID: X-Google-Group-Id: 399137483710 List-Post: , List-Help: , List-Archive: List-Subscribe: , List-Unsubscribe: , Xref: news.gmane.org gmane.comp.lang.c++.isocpp.proposals:4964 Archived-At: ------=_Part_543_24950661.1370884959523 Content-Type: text/plain; charset=ISO-8859-1 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::operator*() precondition{ bool(*this) }; T& optional::operator=(T&&) postcondition{ bool(*this) }; * Compiler should be able to deduce the following: // warning: precondition likely not met *void apply(function f, optional i) { f(*i); } * // safe (checked manually): *void apply1(function f, optional i) { if (i) { f(*i); } }* // safe (postcondition matches the precondition): *void apply2(function f, optional i) { i = 0; f(*i); }* // safe (preferable): *void apply3(function f, optional i) precondition{ bool(i) } { f(*i); }* // no warning, at your own risk: *void apply4(function f, optional i) { [[ satisfied(bool(i)) ]] f(*i); }* // safe (but tricky): *void apply3(function f, optional 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 > PR>* *axiom being_sorted(IT b, IT e, PR p, ValueType v)* *{* * is_sorted(b, e, p) => is_partitioned(b, e, [](auto x){ return p(x, v); });* *}* *template * *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 -- --- 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-proposals+unsubscribe@isocpp.org. To post to this group, send email to std-proposals@isocpp.org. Visit this group at http://groups.google.com/a/isocpp.org/group/std-proposals/?hl=en. ------=_Part_543_24950661.1370884959523 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Hi Everyone,
I wanted to share, and run through the community, one thoug= ht 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=20 assist with static analysis. For instance, given the following=20 pre-/post-conditions for std::optional

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

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

Compiler should be able = to deduce the following:

// warnin= g: precondition likely not met
vo= id apply(function<void(int)> f, optional<int> i)
{
 = f(*i);
}

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

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

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

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

// s= afe (but tricky):
void apply3(function<void(int)> f, optional&l= t;int> i)
{
  if (i =3D=3D nullopt) { i =3D 0; }
  f(= *i);
}

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

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

for instance, if something is sort= ed, it is also partitioned:

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

template <In= tegal I>
axiom being_sorted(I i)
{
  = is_positive(i) =3D> 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 definitio= ns: should Integral be defined first or function is_positive? Also, an axiom may be stated on two different types. In that case, it=20 is not clear in the body of whose type  type the corresponding invaria= nt could should be put:

axiom (XV= ector v, XMatrix m)
{
  v * m <=3D> m * transposed(v); }

You could arbitrarily pick one, but the relation applie= s to both classes.

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

Regards,
&rzej

--
 
---
You received this message because you are subscribed to the Google Groups &= quot;ISO C++ Standard - Future Proposals" group.
To unsubscribe from this group and stop receiving emails from it, send an e= mail to std-proposals+unsubscribe@isocpp.org.
To post to this group, send email to std-proposals@isocpp.org.
Visit this group at http://groups.google.com/a/isocpp.org/group/std-pro= posals/?hl=3Den.
 
 
------=_Part_543_24950661.1370884959523-- .