220 4965 article Path: news.gmane.org!not-for-mail From: Jeffrey Yasskin Newsgroups: gmane.comp.lang.c++.isocpp.proposals Subject: Re: contract programming: invariants or axioms? Date: Mon, 10 Jun 2013 10:47:34 -0700 Lines: 151 Approved: news@gmane.org Message-ID: References: <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: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable X-Trace: ger.gmane.org 1370886477 2347 80.91.229.3 (10 Jun 2013 17:47:57 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Mon, 10 Jun 2013 17:47:57 +0000 (UTC) To: std-proposals@isocpp.org Original-X-From: std-proposals+bncBDDM34EO6QDRBS5C3CGQKGQEKXXQGOA@isocpp.org Mon Jun 10 19:47:58 2013 Return-path: Envelope-to: gclcip-std-proposals@m.gmane.org Original-Received: from mail-ye0-f198.google.com ([209.85.213.198]) by plane.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1Um6CC-0004ca-NM for gclcip-std-proposals@m.gmane.org; Mon, 10 Jun 2013 19:47:56 +0200 Original-Received: by mail-ye0-f198.google.com with SMTP id m13sf6509907yen.5 for ; Mon, 10 Jun 2013 10:47:55 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=20120113; h=x-beenthere:mime-version:in-reply-to:references:from:date :message-id:subject:to:x-original-sender :x-original-authentication-results:reply-to:precedence:mailing-list :list-id:x-google-group-id:list-post:list-help:list-archive :list-subscribe:list-unsubscribe:content-type :content-transfer-encoding; bh=mWtcUJcV42ycuE2Byh3/ewhv1m9Rdf5UOCQpa5DGuSA=; b=MD6K1okzHtKfvg/I4pWCQr2R5SoC++EBRjwGNAhswwbRcycZ7NgZcGPVsmyUbgiaYm IUp1LKnEEi3zzlcZRWYS7NYnvwd+1aHqpSWLPS1AkDisqwjISyqIfbS+ZSDFNPcyxil4 p/8j6EytBg+6JWCLO0fu2grUphchauCZ+GnhaSG6fYlFOih5hMsJ5X9cQhPw7ImUU8SP MA2ED1UH2OaElW7YtfmoeyMpnkDDFM5NIM3mn638HrOpPhAz7DeDM2AFiskuOnLFi7dh Og63Nt9MfZH4RT0LWLWmEJxmoYwGjphtUz2JMMV9hQpckI4+m2y72bU8IQRjIX6+C+50 F X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=google.com; s=20120113; h=x-beenthere:mime-version:in-reply-to:references:from:date :message-id:subject:to:x-gm-message-state:x-original-sender :x-original-authentication-results:reply-to:precedence:mailing-list :list-id:x-google-group-id:list-post:list-help:list-archive :list-subscribe:list-unsubscribe:content-type :content-transfer-encoding; bh=mWtcUJcV42ycuE2Byh3/ewhv1m9Rdf5UOCQpa5DGuSA=; b=d2GtN0Q9IG3rAjrrENfbVyNDhMJmJysmRIYrkN8TVhZCtMEsA4LcpD1QLDxodc5utx aj7+W96txr8+Um/lBmmc/ylyj/JAqBvg5mtBDGvM/ybVvq0ABdAv05XnIetgFsG/ZXbX bBD+ihi8qzOA5hC0hPXhEryIxj6L8ZHnozQgsQ6JGZCR6ZY14/VD78BI6ZpW04aw5c9k DBdSOQYynHsAlSEv7QmulavOw43yLNHEEoGmzEdnmTp8uxKlE9R5SVf9+schqdBp6Fuk eBXVfasaW968gxzMP11S7oHwu1pMqAIqG9UZWbJ0/2yWVhDGrOq X-Received: by 10.224.86.200 with SMTP id t8mr7644053qal.0.1370886475762; Mon, 10 Jun 2013 10:47:55 -0700 (PDT) X-BeenThere: std-proposals@isocpp.org Original-Received: by 10.49.17.134 with SMTP id o6ls2594268qed.33.gmail; Mon, 10 Jun 2013 10:47:54 -0700 (PDT) X-Received: by 10.224.41.3 with SMTP id m3mr14331252qae.53.1370886474500; Mon, 10 Jun 2013 10:47:54 -0700 (PDT) Original-Received: from mail-qa0-x234.google.com (mail-qa0-x234.google.com [2607:f8b0:400d:c00::234]) by mx.google.com with ESMTPS id o10si4536283qcj.158.2013.06.10.10.47.54 for (version=TLSv1 cipher=ECDHE-RSA-RC4-SHA bits=128/128); Mon, 10 Jun 2013 10:47:54 -0700 (PDT) Received-SPF: pass (google.com: domain of jyasskin@google.com designates 2607:f8b0:400d:c00::234 as permitted sender) client-ip=2607:f8b0:400d:c00::234; Original-Received: by mail-qa0-f52.google.com with SMTP id bv4so2458838qab.11 for ; Mon, 10 Jun 2013 10:47:54 -0700 (PDT) X-Received: by 10.49.75.73 with SMTP id a9mr12197572qew.30.1370886474256; Mon, 10 Jun 2013 10:47:54 -0700 (PDT) Original-Received: by 10.229.78.22 with HTTP; Mon, 10 Jun 2013 10:47:34 -0700 (PDT) In-Reply-To: <67dced99-d566-4082-94e1-2f831119e1cf@isocpp.org> X-Gm-Message-State: ALoCoQlbu/JQSbwjq6UozdfOjETlFyKy+615Tdlm+MHvG0b7lXyQjwIGpUYgOdTnS2POjUKY3DklEE0UdSHBbqZEURLMYZ6J/bouBy7azXxbpN6GG6clAcDqlobVlgjB3yWmpUHROmYo4dNx9GmBfhOxhcDkwUoC4jD3ZYnd+O470WpdoYhUTxpEk5pES6XSAruWjqi4UidExQdRA+MuH8HxtNa3VWrJWQ== X-Original-Sender: jyasskin@google.com X-Original-Authentication-Results: mx.google.com; spf=pass (google.com: domain of jyasskin@google.com designates 2607:f8b0:400d:c00::234 as permitted sender) smtp.mail=jyasskin@google.com; dkim=pass header.i=@google.com; dmarc=pass (p=REJECT dis=NONE) d=google.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:4965 Archived-At: 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. On Mon, Jun 10, 2013 at 10:22 AM, Andrzej Krzemie=C5=84ski wrote: > Hi Everyone, > I wanted to share, and run through the community, one thought about contr= act > 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 assis= t > with static analysis. For instance, given the following pre-/post-conditi= ons > for std::optional > > T& optional::operator*() > precondition{ bool(*this) }; > > T& optional::operator=3D(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 =3D 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 =3D=3D nullopt) { i =3D 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) =3D> is_partitioned(b, e, [](auto x){ return p(x, v)= ; }); > } > > template > 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 > definitions: should Integral be defined first or function is_positive? Al= so, > an axiom may be stated on two different types. In that case, it is not cl= ear > in the body of whose type type the corresponding invariant could should = be > put: > > axiom (XVector v, XMatrix m) > { > v * m <=3D> 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 programmi= ng. > 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=3Den. > > --=20 ---=20 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 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-proposa= ls/?hl=3Den. .