220 11721 <6da50966-e3d3-441d-8474-614a51b035df@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: Re: Value constraints (or contract programming in C++) Date: Wed, 9 Jul 2014 01:59:44 -0700 (PDT) Lines: 215 Approved: news@gmane.org Message-ID: <6da50966-e3d3-441d-8474-614a51b035df@isocpp.org> References: Reply-To: std-proposals@isocpp.org NNTP-Posting-Host: plane.gmane.org Mime-Version: 1.0 Content-Type: multipart/alternative; boundary="----=_Part_89_2745534.1404896384615" X-Trace: ger.gmane.org 1404896394 29321 80.91.229.3 (9 Jul 2014 08:59:54 GMT) X-Complaints-To: usenet@ger.gmane.org NNTP-Posting-Date: Wed, 9 Jul 2014 08:59:54 +0000 (UTC) Cc: josedaniel.garcia@uc3m.es To: std-proposals@isocpp.org Original-X-From: std-proposals+bncBDT2DGOJ34DBBAMJ6SOQKGQEUDFF3VI@isocpp.org Wed Jul 09 10:59:47 2014 Return-path: Envelope-to: gclcip-std-proposals@m.gmane.org Original-Received: from mail-vc0-f200.google.com ([209.85.220.200]) by plane.gmane.org with esmtp (Exim 4.69) (envelope-from ) id 1X4nj9-0000A3-2v for gclcip-std-proposals@m.gmane.org; Wed, 09 Jul 2014 10:59:47 +0200 Original-Received: by mail-vc0-f200.google.com with SMTP id id10sf23674066vcb.11 for ; Wed, 09 Jul 2014 01:59:46 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=date:from:to:cc:message-id:in-reply-to:references:subject :mime-version:x-original-sender:reply-to:precedence:mailing-list :list-id:list-post:list-help:list-archive:list-subscribe :list-unsubscribe:content-type; bh=3AAw5pmHHipSobDdoFCTflvBj8cTx0qI768fYWmU/00=; b=IBFDSbFdSvzhxKnUvtX8bUz8eZZOcgVE+lI1NHDWTDCtqf6ej8Mfu/e3BSyCdrw+QE Fj9nwFqpNXXXUxtm2Id7+VpxSW9CKbhpl10nDt5XkBLhMYaQ8l3QhMSSMidvfOmMM7zb Fp3ZpG2/DRYZepxYiN0iKjjL1QWZyLg3Nsu1sPxda14ywTWAY40puL0ZBVCA/+YvznPB joPDLshGUv4192tHH25Js9bysX73Z+dXwY42rpiaCJZE35IDSs4OcUl/HHOpLfszBqh9 xdwrxiMgPpBtNya3oUQVuIIYr/JjvGCGPKOG9B2pLRD9S0uvwwlL1g0enl7eqOs6LVam B+zw== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=x-gm-message-state:date:from:to:cc:message-id:in-reply-to :references:subject:mime-version:x-original-sender:reply-to :precedence:mailing-list:list-id:list-post:list-help:list-archive :list-subscribe:list-unsubscribe:content-type; bh=3AAw5pmHHipSobDdoFCTflvBj8cTx0qI768fYWmU/00=; b=X78x0jGYWwbBxWO35ueXVd9XPFGwgRVwyjZ+LhugajAiiqeVgwWKIehqHpZdjROoOv 2HQU3zr94IVQVP2Lv9NPwd4HmUktghm8Wce4RXx5JgjNN2ViACNOW8KflS8LYUnGVHEe zPUkrFdBWZTN9ZUR9dSp1Gd7jvzRv6mKOcC9BYkk43apUzQT09I3PSx6fPXfVSvLI1dG HKcR1OpJ58EQbQpo3XF4TsaIpIKAKw+Z+UviLXkvOunI6MK6UTgZNHttMkfndb3axacM izq0KpB/SNcno174t180uIrFq+/0y1mAg+oHXKmXQikxVRut1FG0m/zSF271Wb9+aWIJ io7g== X-Gm-Message-State: ALoCoQmPPlbF9S0gj6RWTrHlhc9zpEhiajZuiasupoUE8PWcWbMA7tX1B2MXLE699F9kOs1m3Cay X-Received: by 10.236.189.68 with SMTP id b44mr17559349yhn.4.1404896386144; Wed, 09 Jul 2014 01:59:46 -0700 (PDT) X-BeenThere: std-proposals@isocpp.org Original-Received: by 10.182.28.136 with SMTP id b8ls1206939obh.65.gmail; Wed, 09 Jul 2014 01:59:45 -0700 (PDT) X-Received: by 10.182.243.195 with SMTP id xa3mr202091obc.5.1404896385315; Wed, 09 Jul 2014 01:59:45 -0700 (PDT) In-Reply-To: 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:11721 Archived-At: ------=_Part_89_2745534.1404896384615 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable J. Daniel, I have just learned about your paper. I am about to read it. I= =20 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 Ga= rcia=20 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 par= t=20 >>> of the signature of functions? >>> >> >> Yes but; one of the options is that they are declared as attributes, I a= m=20 >> not sure if it counts as part of function's signature. >> > > Attributes are quite arguable here. Attributes should not have semantic= =20 > effects. However a contract violation checking MAY have semantic effects > I agree that using attributes implies no semantic effects. I am convinced= =20 that the semantics of evaluating preconditions before functions and=20 postconditions after functions is not the only (and not even the most=20 important) use of pre- and post- condition declarations. As an alternative,= =20 they can be used for static analysis and the generation of warning=20 messages, and code optimizations. My ideal is that we first decide what semantics we expect of these=20 correctness declarations: (1) run-time (call precondition before function)= =20 or (2) compile-time (compiler warnings). My choice isn't that obvious in=20 favour of evaluating preconditions at run-time. Once we decide on this, we= =20 can decide on how we want to represent the correctness declarations. If we= =20 decide on (2), [[attributes]] come as a natural choice.=20 =20 > =20 > >> =20 >> >>> If so, does it means that you have to write the contract too when you= =20 >>> forward-declare a free function?=20 >>> >> >> Typically you would declare a function in a header file and define it in= =20 >> a cpp file. In that case you would want to put contract declarations in = a=20 >> header file, when you forward declare a function. >> > > You will want to put the contract in the declaration as it is part of the= =20 > function interface. > > One question here is if all declarations corresponding to the same functi= o=20 > need to have the same contract. i.e should the following be valid code? > > int f(int x); > > int f(int x) > expects(x>0); > > int f(int x)=20 > expects(x>0)=20 > ensures(x>0). > > int f(int x) { > return x*2; > } > > a similar problem was already solved for default function argument=20 declarations, auto type deduction for functions, inline, so we can just=20 copy from the existing solutions. At this point I guess it is of little=20 priority. I agree that correctness declarations are part of function=20 declaration (regardless of whether they affect function signature or=20 overload resolution mechanism or not.) --=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/. ------=_Part_89_2745534.1404896384615 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable

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 dni= u =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 Kr= zemienski <akrz..= ..@gmail.com> wrote:



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

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 attri= butes implies no semantic effects. I am convinced that the semantics of eva= luating preconditions before functions and postconditions after functions i= s not the only (and not even the most important) use of pre- and post- cond= ition declarations. As an alternative, they can be used for static analysis= and the generation of warning messages, and code optimizations.

My = ideal is that we first decide what semantics we expect of  these corre= ctness 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, we can dec= ide on how we want to represent the correctness declarations. If we decide = on (2), [[attributes]] come as a natural choice.
 
 
 
=
If so, does it means that you have to write the contr= act too when you forward-declare a free function? 

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)
  expects(x>0);

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

int f(int x) {
  return x*2;
}


a similar problem was already solv= ed for default function argument declarations, auto type deduction for func= tions, inline, so we can just copy from the existing solutions. At this poi= nt I guess it is of little priority. I agree that correctness declarations = are part of function declaration (regardless of whether they affect functio= n signature or overload resolution mechanism or not.)

--

---
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>.
------=_Part_89_2745534.1404896384615-- .