220 11722 article Path: news.gmane.org!not-for-mail From: "J. Daniel Garcia" Newsgroups: gmane.comp.lang.c++.isocpp.proposals Subject: Re: Value constraints (or contract programming in C++) Date: Wed, 9 Jul 2014 11:19:13 +0200 Lines: 304 Approved: news@gmane.org Message-ID: References: <6da50966-e3d3-441d-8474-614a51b035df@isocpp.org> Reply-To: std-proposals@isocpp.org NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: multipart/alternative; boundary=90e6ba21234706e39b04fdbf36eb X-Trace: ger.gmane.org 1404897605 16014 80.91.229.3 (9 Jul 2014 09:20:05 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 9 Jul 2014 09:20:05 +0000 (UTC) To: std-proposals@isocpp.org Original-X-From: std-proposals+bncBCFIPGWXVYIRBOUS6SOQKGQEF4WMJXY@isocpp.org Wed Jul 09 11:19:58 2014 Return-path: Envelope-to: gclcip-std-proposals@m.gmane.org Original-Received: from mail-ve0-f198.google.com ([209.85.128.198]) by plane.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1X4o2d-0005DE-G6 for gclcip-std-proposals@m.gmane.org; Wed, 09 Jul 2014 11:19:55 +0200 Original-Received: by mail-ve0-f198.google.com with SMTP id db11sf26628157veb.9 for ; Wed, 09 Jul 2014 02:19:54 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=x-gm-message-state:mime-version:sender:in-reply-to:references:from :date:message-id:subject:to:x-original-sender :x-original-authentication-results:reply-to:precedence:mailing-list :list-id:list-post:list-help:list-archive:list-subscribe :list-unsubscribe:content-type; bh=+2UxdVKX+g0WLE3pOKOeeiUlydVORvyWEV/3PCB4ppQ=; b=bALN04AFIA2wtFJezmJufKkZMGfK+keMD8r3Xc8AL0VorR6sd/GeiWBMkLXJ99pwzN faZ3JKjD7T2DyQWWb3NofuzNTW+HH2A5hDpyFrPrcR7O8aR26wk1tCCNB9k2xEEhMCKW vXkIgBP+rWh3OHY0lbEWgzszmyk4As8VIb1Dy8Y5Q1wVHHIPwnsiO8Dk37vLfE83WOfo zFn1m7zfLeNcdtOxtfEn7qAyoF+H3F3vMdaxhOncCnHKHiiN+bbnXXIUOGoJ4uD/IpWj 1nBub0f7+06nxNxVx5McirY/EEDuQ5xno1zpXLIqC59LH9119roQYCx2Qh0w0GXhgAP9 GhOA== X-Gm-Message-State: ALoCoQmcP/ZT+8yysL1VuuBIPLs+Goz1L6KWZKgdS62T9xLs1oy6erIZoHJZ9ZQ0G2b1d/+0wFZD X-Received: by 10.236.31.40 with SMTP id l28mr16928440yha.34.1404897594731; Wed, 09 Jul 2014 02:19:54 -0700 (PDT) X-BeenThere: std-proposals@isocpp.org Original-Received: by 10.50.47.69 with SMTP id b5ls791444ign.15.gmail; Wed, 09 Jul 2014 02:19:53 -0700 (PDT) X-Received: by 10.51.16.132 with SMTP id fw4mr10889542igd.26.1404897593948; Wed, 09 Jul 2014 02:19:53 -0700 (PDT) Original-Received: from mail-ie0-x22e.google.com (mail-ie0-x22e.google.com [2607:f8b0:4001:c03::22e]) by mx.google.com with ESMTPS id e3si7008834igx.4.2014.07.09.02.19.53 for (version=TLSv1 cipher=ECDHE-RSA-RC4-SHA bits=128/128); Wed, 09 Jul 2014 02:19:53 -0700 (PDT) Received-SPF: pass (google.com: domain of josedaniel.garcia.uc3m@gmail.com designates 2607:f8b0:4001:c03::22e as permitted sender) client-ip=2607:f8b0:4001:c03::22e; Original-Received: by mail-ie0-f174.google.com with SMTP id rd18so6050235iec.19 for ; Wed, 09 Jul 2014 02:19:53 -0700 (PDT) X-Received: by 10.42.139.4 with SMTP id e4mr14737644icu.73.1404897593842; Wed, 09 Jul 2014 02:19:53 -0700 (PDT) Original-Sender: josedaniel.garcia.uc3m@gmail.com Original-Received: by 10.64.227.41 with HTTP; Wed, 9 Jul 2014 02:19:13 -0700 (PDT) In-Reply-To: <6da50966-e3d3-441d-8474-614a51b035df@isocpp.org> X-Original-Sender: josedaniel.garcia@uc3m.es X-Original-Authentication-Results: mx.google.com; spf=pass (google.com: domain of josedaniel.garcia.uc3m@gmail.com designates 2607:f8b0:4001:c03::22e as permitted sender) smtp.mail=josedaniel.garcia.uc3m@gmail.com; dkim=pass header.i=@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:11722 Archived-At: --90e6ba21234706e39b04fdbf36eb Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable On Wed, Jul 9, 2014 at 10:59 AM, Andrzej Krzemie=C5=84ski wrote: > > J. Daniel, I have just learned about your paper. I am about to read it. I > am glad that the subject is being pursued. > > W dniu =C5=9Broda, 9 lipca 2014 10:33:15 UTC+2 u=C5=BCytkownik J. Daniel = Garcia > napisa=C5=82: >> >> On Wed, Jul 9, 2014 at 10:24 AM, Andrzej Krzemienski >> wrote: >> >>> >>> >>> >>> 2014-07-08 19:05 GMT+02:00 Klaim - Jo=C3=ABl Lamotte = : >>> >>> Another question: if I understand correctly, the contracts should be >>>> part of the signature of functions? >>>> >>> >>> Yes but; one of the options is that they are declared as attributes, I >>> am not sure if it counts as part of function's signature. >>> >> >> Attributes are quite arguable here. Attributes should not have semantic >> effects. However a contract violation checking MAY have semantic effects >> > > I agree that using attributes implies no semantic effects. I am convinced > that the semantics of evaluating preconditions before functions and > postconditions after functions is not the only (and not even the most > important) use of pre- and post- condition declarations. As an alternativ= e, > they can be used for static analysis and the generation of warning > messages, and code optimizations. > Yes. This are important uses. However, non of them seem a reason to favour attributes. > > My ideal is that we first decide what semantics we expect of these > correctness declarations: (1) run-time (call precondition before function= ) > or (2) compile-time (compiler warnings). My choice isn't that obvious in > favour of evaluating preconditions at run-time. Once we decide on this, w= e > can decide on how we want to represent the correctness declarations. If w= e > decide on (2), [[attributes]] come as a natural choice. > Yes. Representation is secondary. In general, it is unlikely that every assert may be checked at compile-time. Thus, I feel inclined towards run-time checking. However, the compiler should be free of removing checks for those cases where it can be prooved that the assertion never fails. > > >> >> >>> >>> >>>> If so, does it means that you have to write the contract too when you >>>> forward-declare a free function? >>>> >>> >>> Typically you would declare a function in a header file and define it i= n >>> a cpp file. In that case you would want to put contract declarations in= a >>> header file, when you forward declare a function. >>> >> >> You will want to put the contract in the declaration as it is part of th= e >> function interface. >> >> One question here is if all declarations corresponding to the same >> functio need to have the same contract. i.e should the following be vali= d >> code? >> >> int f(int x); >> >> int f(int x) >> expects(x>0); >> >> int f(int x) >> expects(x>0) >> ensures(x>0). >> >> int f(int x) { >> return x*2; >> } >> >> > a similar problem was already solved for default function argument > declarations, auto type deduction for functions, inline, so we can just > copy from the existing solutions. At this point I guess it is of little > priority. I agree that correctness declarations are part of function > declaration (regardless of whether they affect function signature or > overload resolution mechanism or not.) > Agreed! > -- > > --- > 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/. > --=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/. --90e6ba21234706e39b04fdbf36eb Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable

= On Wed, Jul 9, 2014 at 10:59 AM, Andrzej Krzemie=C5=84ski <akrzemi1@gmail= ..com> wrote:

J. Daniel, I have just = learned about your paper. I am about to read it. I am glad that the subject= is being pursued.

W dniu =C5=9Broda, 9 lipca 2014 10:33:15 UTC+2 u=C5=BCytkownik J. Danie= l Garcia napisa=C5=82:
On Wed, Jul 9, 2014 at 10:24 AM, Andrzej Krzemienski <= akrz...@gmail.com> wrote:



2014-07-08 19:05 GMT+02:00 Klaim - Jo=C3=ABl Lamotte <mjk...@gmail.com>:

Another question: if I unde= rstand correctly, the contracts should be part of the signature of function= s?

Yes but; one of the options is that = they are declared as attributes, I am not sure if it counts as part of func= tion's signature.

Attributes are quite arguable here. Attributes should not have s= emantic effects. However a contract violation checking MAY have semantic ef= fects

I agree that using= attributes implies no semantic effects. I am convinced that the semantics = of evaluating preconditions before functions and postconditions after funct= ions is not the only (and not even the most important) use of pre- and post= - condition declarations. As an alternative, they can be used for static an= alysis and the generation of warning messages, and code optimizations.

Yes. This are important uses. = However, non of them seem a reason to favour attributes.
=C2=A0

My ideal is that we first decide what semantics w= e expect of=C2=A0 these correctness declarations: (1) run-time (call precon= dition before function) or (2) compile-time (compiler warnings). My choice = isn't that obvious in favour of evaluating preconditions at run-time. O= nce we decide on this, we can decide on how we want to represent the correc= tness declarations. If we decide on (2), [[attributes]] come as a natural c= hoice.

Yes. Representation is seconda= ry.

In general, it is unlikely that every assert m= ay be checked at compile-time. Thus, I feel inclined towards run-time check= ing. However, the compiler should be free of removing checks for those case= s where it can be prooved that the assertion never fails.

=C2=A0
=C2=A0
=C2=A0
=C2=A0
=
If so, does it means that you have to write the contr= act too when you forward-declare a free function?=C2=A0

Typically you would declare a function in a = header file and define it in a cpp file. In that case you would want to put= contract declarations in a header file, when you forward declare a functio= n.

You will want to p= ut the contract in the declaration as it is part of the function interface.=

One question here is if all declarations correspo= nding to the same functio need to have the same contract. i.e should the fo= llowing be valid code?

int f(int x);

int f(int x)
=C2=A0 expects(x>0);

int f(int x)=C2=A0<= /div>
=C2=A0 expects(x>0)=C2=A0
=C2=A0 ensures(x>0).

int f(int x) {
=C2=A0 return x*2;
}


a similar problem was alread= y solved for default function argument declarations, auto type deduction fo= r functions, inline, so we can just copy from the existing solutions. At th= is point I guess it is of little priority. I agree that correctness declara= tions are part of function declaration (regardless of whether they affect f= unction signature or overload resolution mechanism or not.)

Agreed!=C2=A0

--

---
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/gro= up/std-proposals/.

--

---
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-proposa= ls+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/<= /a>.
--90e6ba21234706e39b04fdbf36eb-- .