Topic: Interaction between contracts and unsupported


Author: jgottman6@gmail.com
Date: Wed, 13 Jun 2018 18:24:37 -0700 (PDT)
Raw View
------=_Part_962_1200890167.1528939477853
Content-Type: multipart/alternative;
 boundary="----=_Part_963_610154122.1528939477853"

------=_Part_963_610154122.1528939477853
Content-Type: text/plain; charset="UTF-8"

Now that contracts have been accepted for C++20, I have a question about
how they interact with templates. Suppose I have a template class like the
following:

template <class X>
class myQueue {
   public:
   const X& back() const;
   void push_back(const X& x)[[ensures: back() == x]];
   //...Other stuff
};

Note the assertion calls operator== on the type X.  But what happens if
this template is instantiated for a type with no operator== ?  Is the
assertion ignored or does the class fail to compile?

Joe Gottman

--
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.
To view this discussion on the web visit https://groups.google.com/a/isocpp.org/d/msgid/std-proposals/d52566a0-3d5f-4bd5-8862-e726255f8eef%40isocpp.org.

------=_Part_963_610154122.1528939477853
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr">Now that contracts have been accepted for C++20, I have a =
question about how they interact with templates. Suppose I have a template =
class like the following:<div><br></div><div><div class=3D"prettyprint" sty=
le=3D"background-color: rgb(250, 250, 250); border-color: rgb(187, 187, 187=
); border-style: solid; border-width: 1px; word-wrap: break-word;"><code cl=
ass=3D"prettyprint"><div class=3D"subprettyprint"><span style=3D"color: #00=
8;" class=3D"styled-by-prettify">template</span><span style=3D"color: #000;=
" class=3D"styled-by-prettify"> </span><span style=3D"color: #660;" class=
=3D"styled-by-prettify">&lt;</span><span style=3D"color: #008;" class=3D"st=
yled-by-prettify">class</span><span style=3D"color: #000;" class=3D"styled-=
by-prettify"> X</span><span style=3D"color: #660;" class=3D"styled-by-prett=
ify">&gt;</span><span style=3D"color: #000;" class=3D"styled-by-prettify"><=
br></span><span style=3D"color: #008;" class=3D"styled-by-prettify">class</=
span><span style=3D"color: #000;" class=3D"styled-by-prettify"> myQueue </s=
pan><span style=3D"color: #660;" class=3D"styled-by-prettify">{</span><span=
 style=3D"color: #000;" class=3D"styled-by-prettify"><br>=C2=A0 =C2=A0</spa=
n><span style=3D"color: #008;" class=3D"styled-by-prettify">public</span><s=
pan style=3D"color: #660;" class=3D"styled-by-prettify">:</span><span style=
=3D"color: #000;" class=3D"styled-by-prettify"><br>=C2=A0 =C2=A0</span><spa=
n style=3D"color: #008;" class=3D"styled-by-prettify">const</span><span sty=
le=3D"color: #000;" class=3D"styled-by-prettify"> X</span><span style=3D"co=
lor: #660;" class=3D"styled-by-prettify">&amp;</span><span style=3D"color: =
#000;" class=3D"styled-by-prettify"> back</span><span style=3D"color: #660;=
" class=3D"styled-by-prettify">()</span><span style=3D"color: #000;" class=
=3D"styled-by-prettify"> </span><span style=3D"color: #008;" class=3D"style=
d-by-prettify">const</span><span style=3D"color: #660;" class=3D"styled-by-=
prettify">;</span><span style=3D"color: #000;" class=3D"styled-by-prettify"=
><br>=C2=A0 =C2=A0</span><span style=3D"color: #008;" class=3D"styled-by-pr=
ettify">void</span><span style=3D"color: #000;" class=3D"styled-by-prettify=
"> push_back</span><span style=3D"color: #660;" class=3D"styled-by-prettify=
">(</span><span style=3D"color: #008;" class=3D"styled-by-prettify">const</=
span><span style=3D"color: #000;" class=3D"styled-by-prettify"> X</span><sp=
an style=3D"color: #660;" class=3D"styled-by-prettify">&amp;</span><span st=
yle=3D"color: #000;" class=3D"styled-by-prettify"> x</span><span style=3D"c=
olor: #660;" class=3D"styled-by-prettify">)[[</span><span style=3D"color: #=
000;" class=3D"styled-by-prettify">ensures</span><span style=3D"color: #660=
;" class=3D"styled-by-prettify">:</span><span style=3D"color: #000;" class=
=3D"styled-by-prettify"> back</span><span style=3D"color: #660;" class=3D"s=
tyled-by-prettify">()</span><span style=3D"color: #000;" class=3D"styled-by=
-prettify"> </span><span style=3D"color: #660;" class=3D"styled-by-prettify=
">=3D=3D</span><span style=3D"color: #000;" class=3D"styled-by-prettify"> x=
</span><span style=3D"color: #660;" class=3D"styled-by-prettify">]];</span>=
<font color=3D"#666600"><span style=3D"color: #000;" class=3D"styled-by-pre=
ttify"><br>=C2=A0 =C2=A0</span><span style=3D"color: #800;" class=3D"styled=
-by-prettify">//...Other stuff</span><span style=3D"color: #000;" class=3D"=
styled-by-prettify"><br></span><span style=3D"color: #660;" class=3D"styled=
-by-prettify">};</span></font><font color=3D"#000000"></font></div></code><=
/div><br>Note the assertion calls operator=3D=3D on the type X.=C2=A0 But w=
hat happens if this template is instantiated for a type with no operator=3D=
=3D ?=C2=A0 Is the assertion ignored or does the class fail to compile?</di=
v><div><br></div><div>Joe Gottman</div></div>

<p></p>

-- <br />
You received this message because you are subscribed to the Google Groups &=
quot;ISO C++ Standard - Future Proposals&quot; group.<br />
To unsubscribe from this group and stop receiving emails from it, send an e=
mail to <a href=3D"mailto:std-proposals+unsubscribe@isocpp.org">std-proposa=
ls+unsubscribe@isocpp.org</a>.<br />
To post to this group, send email to <a href=3D"mailto:std-proposals@isocpp=
..org">std-proposals@isocpp.org</a>.<br />
To view this discussion on the web visit <a href=3D"https://groups.google.c=
om/a/isocpp.org/d/msgid/std-proposals/d52566a0-3d5f-4bd5-8862-e726255f8eef%=
40isocpp.org?utm_medium=3Demail&utm_source=3Dfooter">https://groups.google.=
com/a/isocpp.org/d/msgid/std-proposals/d52566a0-3d5f-4bd5-8862-e726255f8eef=
%40isocpp.org</a>.<br />

------=_Part_963_610154122.1528939477853--

------=_Part_962_1200890167.1528939477853--

.


Author: Nicol Bolas <jmckesson@gmail.com>
Date: Wed, 13 Jun 2018 18:40:28 -0700 (PDT)
Raw View
------=_Part_1038_2114394999.1528940428258
Content-Type: multipart/alternative;
 boundary="----=_Part_1039_759842710.1528940428259"

------=_Part_1039_759842710.1528940428259
Content-Type: text/plain; charset="UTF-8"

On Wednesday, June 13, 2018 at 9:24:37 PM UTC-4, jgot...@gmail.com wrote:
>
> Now that contracts have been accepted for C++20, I have a question about
> how they interact with templates. Suppose I have a template class like the
> following:
>
> template <class X>
> class myQueue {
>    public:
>    const X& back() const;
>    void push_back(const X& x)[[ensures: back() == x]];
>    //...Other stuff
> };
>
> Note the assertion calls operator== on the type X.  But what happens if
> this template is instantiated for a type with no operator== ?  Is the
> assertion ignored or does the class fail to compile?
>
> Joe Gottman
>

The most recent published document on contracts
<http://www.open-std.org/JTC1/SC22/WG21/docs/papers/2018/p0542r4.html> says
that all such expressions are "potentially-evaluated expressions". Which
means that, even if they are never executed, they have to be legitimate. So
if you want to state such a post-condition, then you also need `X` to be
comparable.

Note that `push_back` in the standard library has no such post-condition.

Not all post-conditions or pre-conditions can be fully expressed in the
language, even with the contracts proposal.

--
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.
To view this discussion on the web visit https://groups.google.com/a/isocpp.org/d/msgid/std-proposals/fb285f43-cd12-4004-b282-ee3d4e74dfec%40isocpp.org.

------=_Part_1039_759842710.1528940428259
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr">On Wednesday, June 13, 2018 at 9:24:37 PM UTC-4, jgot...@g=
mail.com wrote:<blockquote class=3D"gmail_quote" style=3D"margin: 0;margin-=
left: 0.8ex;border-left: 1px #ccc solid;padding-left: 1ex;"><div dir=3D"ltr=
">Now that contracts have been accepted for C++20, I have a question about =
how they interact with templates. Suppose I have a template class like the =
following:<div><br></div><div><div style=3D"background-color:rgb(250,250,25=
0);border-color:rgb(187,187,187);border-style:solid;border-width:1px;word-w=
rap:break-word"><code><div><span style=3D"color:#008">template</span><span =
style=3D"color:#000"> </span><span style=3D"color:#660">&lt;</span><span st=
yle=3D"color:#008">class</span><span style=3D"color:#000"> X</span><span st=
yle=3D"color:#660">&gt;</span><span style=3D"color:#000"><br></span><span s=
tyle=3D"color:#008">class</span><span style=3D"color:#000"> myQueue </span>=
<span style=3D"color:#660">{</span><span style=3D"color:#000"><br>=C2=A0 =
=C2=A0</span><span style=3D"color:#008">public</span><span style=3D"color:#=
660">:</span><span style=3D"color:#000"><br>=C2=A0 =C2=A0</span><span style=
=3D"color:#008">const</span><span style=3D"color:#000"> X</span><span style=
=3D"color:#660">&amp;</span><span style=3D"color:#000"> back</span><span st=
yle=3D"color:#660">()</span><span style=3D"color:#000"> </span><span style=
=3D"color:#008">const</span><span style=3D"color:#660">;</span><span style=
=3D"color:#000"><br>=C2=A0 =C2=A0</span><span style=3D"color:#008">void</sp=
an><span style=3D"color:#000"> push_back</span><span style=3D"color:#660">(=
</span><span style=3D"color:#008">const</span><span style=3D"color:#000"> X=
</span><span style=3D"color:#660">&amp;</span><span style=3D"color:#000"> x=
</span><span style=3D"color:#660">)[[</span><span style=3D"color:#000">ensu=
res</span><span style=3D"color:#660">:</span><span style=3D"color:#000"> ba=
ck</span><span style=3D"color:#660">()</span><span style=3D"color:#000"> </=
span><span style=3D"color:#660">=3D=3D</span><span style=3D"color:#000"> x<=
/span><span style=3D"color:#660">]];</span><font color=3D"#666600"><span st=
yle=3D"color:#000"><br>=C2=A0 =C2=A0</span><span style=3D"color:#800">//...=
Other stuff</span><span style=3D"color:#000"><br></span><span style=3D"colo=
r:#660">};</span></font><font color=3D"#000000"></font></div></code></div><=
br>Note the assertion calls operator=3D=3D on the type X.=C2=A0 But what ha=
ppens if this template is instantiated for a type with no operator=3D=3D ?=
=C2=A0 Is the assertion ignored or does the class fail to compile?</div><di=
v><br></div><div>Joe Gottman</div></div></blockquote><div><br></div><div>Th=
e <a href=3D"http://www.open-std.org/JTC1/SC22/WG21/docs/papers/2018/p0542r=
4.html">most recent published document on contracts</a> says that all such =
expressions are &quot;potentially-evaluated expressions&quot;. Which means =
that, even if they are never executed, they have to be legitimate. So if yo=
u want to state such a post-condition, then you also need `X` to be compara=
ble.</div><div><br></div><div>Note that `push_back` in the standard library=
 has no such post-condition.</div><div><br></div><div>Not all post-conditio=
ns or pre-conditions can be fully expressed in the language, even with the =
contracts proposal.<br></div></div>

<p></p>

-- <br />
You received this message because you are subscribed to the Google Groups &=
quot;ISO C++ Standard - Future Proposals&quot; group.<br />
To unsubscribe from this group and stop receiving emails from it, send an e=
mail to <a href=3D"mailto:std-proposals+unsubscribe@isocpp.org">std-proposa=
ls+unsubscribe@isocpp.org</a>.<br />
To post to this group, send email to <a href=3D"mailto:std-proposals@isocpp=
..org">std-proposals@isocpp.org</a>.<br />
To view this discussion on the web visit <a href=3D"https://groups.google.c=
om/a/isocpp.org/d/msgid/std-proposals/fb285f43-cd12-4004-b282-ee3d4e74dfec%=
40isocpp.org?utm_medium=3Demail&utm_source=3Dfooter">https://groups.google.=
com/a/isocpp.org/d/msgid/std-proposals/fb285f43-cd12-4004-b282-ee3d4e74dfec=
%40isocpp.org</a>.<br />

------=_Part_1039_759842710.1528940428259--

------=_Part_1038_2114394999.1528940428258--

.


Author: Richard Smith <richard@metafoo.co.uk>
Date: Thu, 14 Jun 2018 21:26:20 -0700
Raw View
--000000000000e2c92f056ea69efb
Content-Type: text/plain; charset="UTF-8"

On Wed, 13 Jun 2018, 18:24 , <jgottman6@gmail.com> wrote:

> Now that contracts have been accepted for C++20, I have a question about
> how they interact with templates. Suppose I have a template class like the
> following:
>
> template <class X>
> class myQueue {
>    public:
>    const X& back() const;
>    void push_back(const X& x)[[ensures: back() == x]];
>    //...Other stuff
> };
>
> Note the assertion calls operator== on the type X.  But what happens if
> this template is instantiated for a type with no operator== ?  Is the
> assertion ignored or does the class fail to compile?
>

We discussed this when reviewing the wording and decided that substitution
should happen eagerly, which means instantiation of the class would fail in
the situation you describe.

Joe Gottman
>
> --
> 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.
> To view this discussion on the web visit
> https://groups.google.com/a/isocpp.org/d/msgid/std-proposals/d52566a0-3d5f-4bd5-8862-e726255f8eef%40isocpp.org
> <https://groups.google.com/a/isocpp.org/d/msgid/std-proposals/d52566a0-3d5f-4bd5-8862-e726255f8eef%40isocpp.org?utm_medium=email&utm_source=footer>
> .
>

--
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.
To view this discussion on the web visit https://groups.google.com/a/isocpp.org/d/msgid/std-proposals/CAOfiQqmp6%3DqQTvXRmDL7PaMVuyg0-JB7p9cDNi7Xqp5qSC7wkw%40mail.gmail.com.

--000000000000e2c92f056ea69efb
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

<div dir=3D"auto"><div><div class=3D"gmail_quote"><div dir=3D"ltr">On Wed, =
13 Jun 2018, 18:24 , &lt;<a href=3D"mailto:jgottman6@gmail.com">jgottman6@g=
mail.com</a>&gt; wrote:<br></div><blockquote class=3D"gmail_quote" style=3D=
"margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir=3D=
"ltr">Now that contracts have been accepted for C++20, I have a question ab=
out how they interact with templates. Suppose I have a template class like =
the following:<div><br></div><div><div class=3D"m_-627932335287668385pretty=
print" style=3D"background-color:rgb(250,250,250);border-color:rgb(187,187,=
187);border-style:solid;border-width:1px;word-wrap:break-word"><code class=
=3D"m_-627932335287668385prettyprint"><div class=3D"m_-627932335287668385su=
bprettyprint"><span style=3D"color:#008" class=3D"m_-627932335287668385styl=
ed-by-prettify">template</span><span style=3D"color:#000" class=3D"m_-62793=
2335287668385styled-by-prettify"> </span><span style=3D"color:#660" class=
=3D"m_-627932335287668385styled-by-prettify">&lt;</span><span style=3D"colo=
r:#008" class=3D"m_-627932335287668385styled-by-prettify">class</span><span=
 style=3D"color:#000" class=3D"m_-627932335287668385styled-by-prettify"> X<=
/span><span style=3D"color:#660" class=3D"m_-627932335287668385styled-by-pr=
ettify">&gt;</span><span style=3D"color:#000" class=3D"m_-62793233528766838=
5styled-by-prettify"><br></span><span style=3D"color:#008" class=3D"m_-6279=
32335287668385styled-by-prettify">class</span><span style=3D"color:#000" cl=
ass=3D"m_-627932335287668385styled-by-prettify"> myQueue </span><span style=
=3D"color:#660" class=3D"m_-627932335287668385styled-by-prettify">{</span><=
span style=3D"color:#000" class=3D"m_-627932335287668385styled-by-prettify"=
><br>=C2=A0 =C2=A0</span><span style=3D"color:#008" class=3D"m_-62793233528=
7668385styled-by-prettify">public</span><span style=3D"color:#660" class=3D=
"m_-627932335287668385styled-by-prettify">:</span><span style=3D"color:#000=
" class=3D"m_-627932335287668385styled-by-prettify"><br>=C2=A0 =C2=A0</span=
><span style=3D"color:#008" class=3D"m_-627932335287668385styled-by-prettif=
y">const</span><span style=3D"color:#000" class=3D"m_-627932335287668385sty=
led-by-prettify"> X</span><span style=3D"color:#660" class=3D"m_-6279323352=
87668385styled-by-prettify">&amp;</span><span style=3D"color:#000" class=3D=
"m_-627932335287668385styled-by-prettify"> back</span><span style=3D"color:=
#660" class=3D"m_-627932335287668385styled-by-prettify">()</span><span styl=
e=3D"color:#000" class=3D"m_-627932335287668385styled-by-prettify"> </span>=
<span style=3D"color:#008" class=3D"m_-627932335287668385styled-by-prettify=
">const</span><span style=3D"color:#660" class=3D"m_-627932335287668385styl=
ed-by-prettify">;</span><span style=3D"color:#000" class=3D"m_-627932335287=
668385styled-by-prettify"><br>=C2=A0 =C2=A0</span><span style=3D"color:#008=
" class=3D"m_-627932335287668385styled-by-prettify">void</span><span style=
=3D"color:#000" class=3D"m_-627932335287668385styled-by-prettify"> push_bac=
k</span><span style=3D"color:#660" class=3D"m_-627932335287668385styled-by-=
prettify">(</span><span style=3D"color:#008" class=3D"m_-627932335287668385=
styled-by-prettify">const</span><span style=3D"color:#000" class=3D"m_-6279=
32335287668385styled-by-prettify"> X</span><span style=3D"color:#660" class=
=3D"m_-627932335287668385styled-by-prettify">&amp;</span><span style=3D"col=
or:#000" class=3D"m_-627932335287668385styled-by-prettify"> x</span><span s=
tyle=3D"color:#660" class=3D"m_-627932335287668385styled-by-prettify">)[[</=
span><span style=3D"color:#000" class=3D"m_-627932335287668385styled-by-pre=
ttify">ensures</span><span style=3D"color:#660" class=3D"m_-627932335287668=
385styled-by-prettify">:</span><span style=3D"color:#000" class=3D"m_-62793=
2335287668385styled-by-prettify"> back</span><span style=3D"color:#660" cla=
ss=3D"m_-627932335287668385styled-by-prettify">()</span><span style=3D"colo=
r:#000" class=3D"m_-627932335287668385styled-by-prettify"> </span><span sty=
le=3D"color:#660" class=3D"m_-627932335287668385styled-by-prettify">=3D=3D<=
/span><span style=3D"color:#000" class=3D"m_-627932335287668385styled-by-pr=
ettify"> x</span><span style=3D"color:#660" class=3D"m_-627932335287668385s=
tyled-by-prettify">]];</span><font color=3D"#666600"><span style=3D"color:#=
000" class=3D"m_-627932335287668385styled-by-prettify"><br>=C2=A0 =C2=A0</s=
pan><span style=3D"color:#800" class=3D"m_-627932335287668385styled-by-pret=
tify">//...Other stuff</span><span style=3D"color:#000" class=3D"m_-6279323=
35287668385styled-by-prettify"><br></span><span style=3D"color:#660" class=
=3D"m_-627932335287668385styled-by-prettify">};</span></font><font color=3D=
"#000000"></font></div></code></div><br>Note the assertion calls operator=
=3D=3D on the type X.=C2=A0 But what happens if this template is instantiat=
ed for a type with no operator=3D=3D ?=C2=A0 Is the assertion ignored or do=
es the class fail to compile?</div></div></blockquote></div></div><div dir=
=3D"auto"><br></div><div dir=3D"auto">We discussed this when reviewing the =
wording and decided that substitution should happen eagerly, which means in=
stantiation of the class would fail in the situation you describe.</div><di=
v dir=3D"auto"><br></div><div dir=3D"auto"><div class=3D"gmail_quote"><bloc=
kquote class=3D"gmail_quote" style=3D"margin:0 0 0 .8ex;border-left:1px #cc=
c solid;padding-left:1ex"><div dir=3D"ltr"><div>Joe Gottman</div></div>

<p></p>

-- <br>
You received this message because you are subscribed to the Google Groups &=
quot;ISO C++ Standard - Future Proposals&quot; group.<br>
To unsubscribe from this group and stop receiving emails from it, send an e=
mail to <a href=3D"mailto:std-proposals+unsubscribe@isocpp.org" target=3D"_=
blank" rel=3D"noreferrer">std-proposals+unsubscribe@isocpp.org</a>.<br>
To post to this group, send email to <a href=3D"mailto:std-proposals@isocpp=
..org" target=3D"_blank" rel=3D"noreferrer">std-proposals@isocpp.org</a>.<br=
>
To view this discussion on the web visit <a href=3D"https://groups.google.c=
om/a/isocpp.org/d/msgid/std-proposals/d52566a0-3d5f-4bd5-8862-e726255f8eef%=
40isocpp.org?utm_medium=3Demail&amp;utm_source=3Dfooter" target=3D"_blank" =
rel=3D"noreferrer">https://groups.google.com/a/isocpp.org/d/msgid/std-propo=
sals/d52566a0-3d5f-4bd5-8862-e726255f8eef%40isocpp.org</a>.<br>
</blockquote></div></div></div>

<p></p>

-- <br />
You received this message because you are subscribed to the Google Groups &=
quot;ISO C++ Standard - Future Proposals&quot; group.<br />
To unsubscribe from this group and stop receiving emails from it, send an e=
mail to <a href=3D"mailto:std-proposals+unsubscribe@isocpp.org">std-proposa=
ls+unsubscribe@isocpp.org</a>.<br />
To post to this group, send email to <a href=3D"mailto:std-proposals@isocpp=
..org">std-proposals@isocpp.org</a>.<br />
To view this discussion on the web visit <a href=3D"https://groups.google.c=
om/a/isocpp.org/d/msgid/std-proposals/CAOfiQqmp6%3DqQTvXRmDL7PaMVuyg0-JB7p9=
cDNi7Xqp5qSC7wkw%40mail.gmail.com?utm_medium=3Demail&utm_source=3Dfooter">h=
ttps://groups.google.com/a/isocpp.org/d/msgid/std-proposals/CAOfiQqmp6%3DqQ=
TvXRmDL7PaMVuyg0-JB7p9cDNi7Xqp5qSC7wkw%40mail.gmail.com</a>.<br />

--000000000000e2c92f056ea69efb--

.