------=_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<T>::operator*()
precondition{ bool(*this) };

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

Compiler should be able to deduce the following:

// warning: precondition likely not met
*void apply(function<void(int)> f, optional<int> i)
{
  f(*i);
}
*
// safe (checked manually):
*void apply1(function<void(int)> f, optional<int> i)
{
  if (i) { f(*i); }
}*

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

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

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

// safe (but tricky):
*void apply3(function<void(int)> f, optional<int> 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<http://www.open-std.org/Jtc1/SC22/wg21/docs/papers/2009/n2887.pdf>).
The latter appears a more universal choice.

for instance, if something is sorted, it is also partitioned:

*template <ForwardIterator IT, BinaryPredicate<ValueType<IT>> PR>*
*axiom being_sorted(IT b, IT e, PR p, ValueType<IT> v)*
*{*
*  is_sorted(b, e, p) => is_partitioned(b, e, [](auto x){ return p(x, v);
});*
*}*

*template <Integal I>*
*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,<br>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.<br><br>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 <b>std::optional</b><br><b><br></b><div style=3D"m=
argin-left: 40px;"><b>T&amp; optional&lt;T&gt;::operator*()<br>precondition=
{ bool(*this) };<br><br>T&amp; optional&lt;T&gt;::operator=3D(T&amp;&amp;)<=
br>postcondition{ bool(*this) }; </b><br><br></div>Compiler should be able =
to deduce the following:<br><br><div style=3D"margin-left: 40px;">// warnin=
g: precondition likely not met</div><div style=3D"margin-left: 40px;"><b>vo=
id apply(function&lt;void(int)&gt; f, optional&lt;int&gt; i)<br>{<br>&nbsp;=
 f(*i);<br>}<br></b><br>// safe (checked manually):<br><b>void apply1(funct=
ion&lt;void(int)&gt; f, optional&lt;int&gt; i)<br>{<br>&nbsp; if (i) { f(*i=
); }<br>}</b><br><br>// safe (postcondition matches the precondition):<br><=
b>void apply2(function&lt;void(int)&gt; f, optional&lt;int&gt; i)<br>{<br>&=
nbsp; i =3D 0;<br>&nbsp; f(*i);<br>}</b><br><br>// safe (preferable):<br><b=
>void apply3(function&lt;void(int)&gt; f, optional&lt;int&gt; i)<br>precond=
ition{ bool(i) }<br>{<br>&nbsp; f(*i);<br>}</b><br><br>// no warning, at yo=
ur own risk:<br><b>void apply4(function&lt;void(int)&gt; f, optional&lt;int=
&gt; i)<br>{<br>&nbsp; [[ satisfied(bool(i)) ]] f(*i);<br>}</b><br><br>// s=
afe (but tricky):<br><b>void apply3(function&lt;void(int)&gt; f, optional&l=
t;int&gt; i)<br>{<br>&nbsp; if (i =3D=3D nullopt) { i =3D 0; }<br>&nbsp; f(=
*i);<br>}</b><br><br></div>"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.<br><br>The last example is problematic: how should the compiler kn=
ow that contextual conversion to <b>bool </b>and the comparison against <b>=
nullopt </b>are 'compatible'? This could be done with an invariant, but cou=
ld as well be done with an axiom (as described in <a href=3D"http://www.ope=
n-std.org/Jtc1/SC22/wg21/docs/papers/2009/n2887.pdf">N2887</a>). The latter=
 appears a more universal choice.<br><br>for instance, if something is sort=
ed, it is also partitioned:<br><br><div style=3D"margin-left: 40px;"><b>tem=
plate &lt;ForwardIterator IT, BinaryPredicate&lt;ValueType&lt;IT&gt;&gt; PR=
&gt;</b><br><b>axiom being_sorted(IT b, IT e, PR p, ValueType&lt;IT&gt; v)<=
/b><br><b>{</b><br><b>&nbsp; is_sorted(b, e, p) =3D&gt; is_partitioned(b, e=
, [](auto x){ return p(x, v); });</b><br><b>}</b><br><br><b>template &lt;In=
tegal I&gt;</b><br><b>axiom being_sorted(I i)</b><br><b>{</b><br><b>&nbsp; =
is_positive(i) =3D&gt; is_nonnegative(i);</b><br><b>}</b><br><br></div>This=
 could be expressed as an invariant:<br><br><div style=3D"margin-left: 40px=
;"><b>class Integral {<br>&nbsp; invariant {<br>&nbsp; &nbsp; !is_positive(=
*this) || is_nonnegative(*this);<br>&nbsp; }<br>};<br></b><br></div>But it =
looks more like a hack and puts some restrictions on the order of definitio=
ns: should <b>Integral </b>be defined first or function <b>is_positive</b>?
 Also, an axiom may be stated on two different types. In that case, it=20
is not clear in the body of whose type&nbsp; type the corresponding invaria=
nt
 could should be put:<br><br><div style=3D"margin-left: 40px;"><b>axiom (XV=
ector v, XMatrix m)<br>{<br>&nbsp; v * m &lt;=3D&gt; m * transposed(v); <br=
>}</b><br><br></div>You could arbitrarily pick one, but the relation applie=
s to both classes.<br><br>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.<br><br>Regards,<br>&amp;rzej<br>

<p></p>

-- <br />
&nbsp;<br />
--- <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 std-proposals+unsubscribe@isocpp.org.<br />
To post to this group, send email to std-proposals@isocpp.org.<br />
Visit this group at <a href=3D"http://groups.google.com/a/isocpp.org/group/=
std-proposals/?hl=3Den">http://groups.google.com/a/isocpp.org/group/std-pro=
posals/?hl=3Den</a>.<br />
&nbsp;<br />
&nbsp;<br />

------=_Part_543_24950661.1370884959523--

.

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
<akrzemi1@gmail.com> 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<T>::operator*()
> precondition{ bool(*this) };
>
> T& optional<T>::operator=3D(T&&)
> postcondition{ bool(*this) };
>
> Compiler should be able to deduce the following:
>
> // warning: precondition likely not met
> void apply(function<void(int)> f, optional<int> i)
> {
>   f(*i);
> }
>
> // safe (checked manually):
> void apply1(function<void(int)> f, optional<int> i)
> {
>   if (i) { f(*i); }
> }
>
> // safe (postcondition matches the precondition):
> void apply2(function<void(int)> f, optional<int> i)
> {
>   i =3D 0;
>   f(*i);
> }
>
> // safe (preferable):
> void apply3(function<void(int)> f, optional<int> i)
> precondition{ bool(i) }
> {
>   f(*i);
> }
>
> // no warning, at your own risk:
> void apply4(function<void(int)> f, optional<int> i)
> {
>   [[ satisfied(bool(i)) ]] f(*i);
> }
>
> // safe (but tricky):
> void apply3(function<void(int)> f, optional<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
> 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 <ForwardIterator IT, BinaryPredicate<ValueType<IT>> PR>
> axiom being_sorted(IT b, IT e, PR p, ValueType<IT> v)
> {
>   is_sorted(b, e, p) =3D> is_partitioned(b, e, [](auto x){ return p(x, v)=
; });
> }
>
> template <Integal 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
> 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.



.

--001a11c1a4b470bbd904ded0a25d
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: quoted-printable

Might be worthwhile to take a look at the Assertion Definition Language:
http://adl.opengroup.org/

Tony


On Mon, Jun 10, 2013 at 1:47 PM, Jeffrey Yasskin <jyasskin@google.com>wrote=
:

> 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
> <akrzemi1@gmail.com> wrote:
> > 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<T>::operator*()
> > precondition{ bool(*this) };
> >
> > T& optional<T>::operator=3D(T&&)
> > postcondition{ bool(*this) };
> >
> > Compiler should be able to deduce the following:
> >
> > // warning: precondition likely not met
> > void apply(function<void(int)> f, optional<int> i)
> > {
> >   f(*i);
> > }
> >
> > // safe (checked manually):
> > void apply1(function<void(int)> f, optional<int> i)
> > {
> >   if (i) { f(*i); }
> > }
> >
> > // safe (postcondition matches the precondition):
> > void apply2(function<void(int)> f, optional<int> i)
> > {
> >   i =3D 0;
> >   f(*i);
> > }
> >
> > // safe (preferable):
> > void apply3(function<void(int)> f, optional<int> i)
> > precondition{ bool(i) }
> > {
> >   f(*i);
> > }
> >
> > // no warning, at your own risk:
> > void apply4(function<void(int)> f, optional<int> i)
> > {
> >   [[ satisfied(bool(i)) ]] f(*i);
> > }
> >
> > // safe (but tricky):
> > void apply3(function<void(int)> f, optional<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
> > changed asynchronously?) but still it allows a certain degree of comfor=
t.
> >
> > 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 b=
e
> > 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 <ForwardIterator IT, BinaryPredicate<ValueType<IT>> PR>
> > axiom being_sorted(IT b, IT e, PR p, ValueType<IT> v)
> > {
> >   is_sorted(b, e, p) =3D> is_partitioned(b, e, [](auto x){ return p(x, =
v);
> });
> > }
> >
> > template <Integal 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 o=
f
> > 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 shoul=
d
> be
> > put:
> >
> > axiom (XVector v, XMatrix m)
> > {
> >   v * m <=3D> m * transposed(v);
> > }
> >
> > You could arbitrarily pick one, but the relation applies to both classe=
s.
> >
> > 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 Grou=
ps
> > "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.
> >
> >
>
> --
>
> ---
> 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.



--001a11c1a4b470bbd904ded0a25d
Content-Type: text/html; charset=UTF-8
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr"><div>Might be worthwhile to take a look at the Assertion D=
efinition Language: <a href=3D"http://adl.opengroup.org/">http://adl.opengr=
oup.org/</a><br><br></div>Tony<br></div><div class=3D"gmail_extra"><br><br>=
<div class=3D"gmail_quote">
On Mon, Jun 10, 2013 at 1:47 PM, Jeffrey Yasskin <span dir=3D"ltr">&lt;<a h=
ref=3D"mailto:jyasskin@google.com" target=3D"_blank">jyasskin@google.com</a=
>&gt;</span> wrote:<br><blockquote class=3D"gmail_quote" style=3D"margin:0 =
0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
Do you have any examples of static analysis tools that are helped in<br>
practice by either declared invariants or declared axioms? I hear a<br>
lot of claims from the contract programming crowd that invariants and<br>
axioms should help static analysis, but I&#39;ve heard very little from<br>
the people actually writing such tools. I really want their experience<br>
to drive whatever design C++ moves toward.<br>
<div class=3D"HOEnZb"><div class=3D"h5"><br>
On Mon, Jun 10, 2013 at 10:22 AM, Andrzej Krzemie=C5=84ski<br>
&lt;<a href=3D"mailto:akrzemi1@gmail.com">akrzemi1@gmail.com</a>&gt; wrote:=
<br>
&gt; Hi Everyone,<br>
&gt; I wanted to share, and run through the community, one thought about co=
ntract<br>
&gt; programming features. Namely, that axioms (like those in concepts) are=
 a<br>
&gt; superior alternative to invariants.<br>
&gt;<br>
&gt; One of the goals of contract programming support in C++ would be to as=
sist<br>
&gt; with static analysis. For instance, given the following pre-/post-cond=
itions<br>
&gt; for std::optional<br>
&gt;<br>
&gt; T&amp; optional&lt;T&gt;::operator*()<br>
&gt; precondition{ bool(*this) };<br>
&gt;<br>
&gt; T&amp; optional&lt;T&gt;::operator=3D(T&amp;&amp;)<br>
&gt; postcondition{ bool(*this) };<br>
&gt;<br>
&gt; Compiler should be able to deduce the following:<br>
&gt;<br>
&gt; // warning: precondition likely not met<br>
&gt; void apply(function&lt;void(int)&gt; f, optional&lt;int&gt; i)<br>
&gt; {<br>
&gt; =C2=A0 f(*i);<br>
&gt; }<br>
&gt;<br>
&gt; // safe (checked manually):<br>
&gt; void apply1(function&lt;void(int)&gt; f, optional&lt;int&gt; i)<br>
&gt; {<br>
&gt; =C2=A0 if (i) { f(*i); }<br>
&gt; }<br>
&gt;<br>
&gt; // safe (postcondition matches the precondition):<br>
&gt; void apply2(function&lt;void(int)&gt; f, optional&lt;int&gt; i)<br>
&gt; {<br>
&gt; =C2=A0 i =3D 0;<br>
&gt; =C2=A0 f(*i);<br>
&gt; }<br>
&gt;<br>
&gt; // safe (preferable):<br>
&gt; void apply3(function&lt;void(int)&gt; f, optional&lt;int&gt; i)<br>
&gt; precondition{ bool(i) }<br>
&gt; {<br>
&gt; =C2=A0 f(*i);<br>
&gt; }<br>
&gt;<br>
&gt; // no warning, at your own risk:<br>
&gt; void apply4(function&lt;void(int)&gt; f, optional&lt;int&gt; i)<br>
&gt; {<br>
&gt; =C2=A0 [[ satisfied(bool(i)) ]] f(*i);<br>
&gt; }<br>
&gt;<br>
&gt; // safe (but tricky):<br>
&gt; void apply3(function&lt;void(int)&gt; f, optional&lt;int&gt; i)<br>
&gt; {<br>
&gt; =C2=A0 if (i =3D=3D nullopt) { i =3D 0; }<br>
&gt; =C2=A0 f(*i);<br>
&gt; }<br>
&gt;<br>
&gt; &quot;Safe&quot; is not a guarantee that the precondition would hold (=
what if value is<br>
&gt; changed asynchronously?) but still it allows a certain degree of comfo=
rt.<br>
&gt;<br>
&gt; The last example is problematic: how should the compiler know that<br>
&gt; contextual conversion to bool and the comparison against nullopt are<b=
r>
&gt; &#39;compatible&#39;? This could be done with an invariant, but could =
as well be<br>
&gt; done with an axiom (as described in N2887). The latter appears a more<=
br>
&gt; universal choice.<br>
&gt;<br>
&gt; for instance, if something is sorted, it is also partitioned:<br>
&gt;<br>
&gt; template &lt;ForwardIterator IT, BinaryPredicate&lt;ValueType&lt;IT&gt=
;&gt; PR&gt;<br>
&gt; axiom being_sorted(IT b, IT e, PR p, ValueType&lt;IT&gt; v)<br>
&gt; {<br>
&gt; =C2=A0 is_sorted(b, e, p) =3D&gt; is_partitioned(b, e, [](auto x){ ret=
urn p(x, v); });<br>
&gt; }<br>
&gt;<br>
&gt; template &lt;Integal I&gt;<br>
&gt; axiom being_sorted(I i)<br>
&gt; {<br>
&gt; =C2=A0 is_positive(i) =3D&gt; is_nonnegative(i);<br>
&gt; }<br>
&gt;<br>
&gt; This could be expressed as an invariant:<br>
&gt;<br>
&gt; class Integral {<br>
&gt; =C2=A0 invariant {<br>
&gt; =C2=A0 =C2=A0 !is_positive(*this) || is_nonnegative(*this);<br>
&gt; =C2=A0 }<br>
&gt; };<br>
&gt;<br>
&gt; But it looks more like a hack and puts some restrictions on the order =
of<br>
&gt; definitions: should Integral be defined first or function is_positive?=
 Also,<br>
&gt; an axiom may be stated on two different types. In that case, it is not=
 clear<br>
&gt; in the body of whose type =C2=A0type the corresponding invariant could=
 should be<br>
&gt; put:<br>
&gt;<br>
&gt; axiom (XVector v, XMatrix m)<br>
&gt; {<br>
&gt; =C2=A0 v * m &lt;=3D&gt; m * transposed(v);<br>
&gt; }<br>
&gt;<br>
&gt; You could arbitrarily pick one, but the relation applies to both class=
es.<br>
&gt;<br>
&gt; It looks to me that axioms are a generalization (or a superset) or<br>
&gt; invariants. Perhaps they should be an integral part of contract progra=
mming.<br>
&gt; I wonder what others think.<br>
&gt;<br>
&gt; Regards,<br>
&gt; &amp;rzej<br>
&gt;<br>
&gt; --<br>
&gt;<br>
&gt; ---<br>
&gt; You received this message because you are subscribed to the Google Gro=
ups<br>
&gt; &quot;ISO C++ Standard - Future Proposals&quot; group.<br>
&gt; To unsubscribe from this group and stop receiving emails from it, send=
 an<br>
&gt; email to <a href=3D"mailto:std-proposals%2Bunsubscribe@isocpp.org">std=
-proposals+unsubscribe@isocpp.org</a>.<br>
&gt; To post to this group, send email to <a href=3D"mailto:std-proposals@i=
socpp.org">std-proposals@isocpp.org</a>.<br>
&gt; Visit this group at<br>
&gt; <a href=3D"http://groups.google.com/a/isocpp.org/group/std-proposals/?=
hl=3Den" target=3D"_blank">http://groups.google.com/a/isocpp.org/group/std-=
proposals/?hl=3Den</a>.<br>
&gt;<br>
&gt;<br>
<br>
--<br>
<br>
---<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%2Bunsubscribe@isocpp.org">std-propo=
sals+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>
Visit this group at <a href=3D"http://groups.google.com/a/isocpp.org/group/=
std-proposals/?hl=3Den" target=3D"_blank">http://groups.google.com/a/isocpp=
..org/group/std-proposals/?hl=3Den</a>.<br>
<br>
<br>
</div></div></blockquote></div><br></div>

<p></p>

-- <br />
&nbsp;<br />
--- <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 std-proposals+unsubscribe@isocpp.org.<br />
To post to this group, send email to std-proposals@isocpp.org.<br />
Visit this group at <a href=3D"http://groups.google.com/a/isocpp.org/group/=
std-proposals/?hl=3Den">http://groups.google.com/a/isocpp.org/group/std-pro=
posals/?hl=3Den</a>.<br />
&nbsp;<br />
&nbsp;<br />

--001a11c1a4b470bbd904ded0a25d--

.

On 6/10/13, Andrzej Krzemie=C5=84ski <akrzemi1@gmail.com> wrote:
> 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.

You are probably right, but I wonder if generalizing that way is
going to exceed our experience.  That is, do you think it possible
or reasonable to define the simpler form, get use experience, and
then extend?

--=20
Lawrence Crowl

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



.

On 6/10/13, Jeffrey Yasskin <jyasskin@google.com> wrote:
> 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.

Sun's compiler had pragmas that looked alot like invariants.  They
we pretty simple, like count < n or count % 4 == 0.  The optimizer
used them to guide optimization and strip out unnecessary code.

The problem was that the syntax was not portable.  Programmers do
not want to spend a lot of time on platform-specific annotations
if they can avoid it.  So, it didn't get used much.

I don't know that we have much experience chaining the postcondition
from on call into the preconditions of another call, but having that
information would certainly let static analysis programs point out
when the code looks incomplete.

I think we are in a bit of a bind here.  Without a standard syntax
for saying such things, no one will properly develop the tools.

--
Lawrence Crowl

--

---
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.



.

On Tue, Jun 11, 2013 at 8:47 PM, Lawrence Crowl <crowl@googlers.com> wrote:
> On 6/10/13, Jeffrey Yasskin <jyasskin@google.com> wrote:
>> 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.
>
> Sun's compiler had pragmas that looked alot like invariants.  They
> we pretty simple, like count < n or count % 4 == 0.  The optimizer
> used them to guide optimization and strip out unnecessary code.
>
> The problem was that the syntax was not portable.  Programmers do
> not want to spend a lot of time on platform-specific annotations
> if they can avoid it.  So, it didn't get used much.
>
> I don't know that we have much experience chaining the postcondition
> from on call into the preconditions of another call, but having that
> information would certainly let static analysis programs point out
> when the code looks incomplete.
>
> I think we are in a bit of a bind here.  Without a standard syntax
> for saying such things, no one will properly develop the tools.

People used 'override' when it was just Microsoft, and we're using
[[clang::fallthrough]] even though it's just clang. People in
companies that use Coverity or Klocwork are just as likely to be
willing to add annotations that would make those tools work better. If
those companies haven't come up with such annotations, that's a mark
against trying to invent something for them to use.

--

---
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_443_6160953.1371194701707
Content-Type: text/plain; charset=ISO-8859-2
Content-Transfer-Encoding: quoted-printable



W dniu =B6roda, 12 czerwca 2013 05:42:38 UTC+2 u=BFytkownik Lawrence Crowl=
=20
napisa=B3:
>
> On 6/10/13, Andrzej Krzemie=F1ski <akrz...@gmail.com <javascript:>> wrote=
:=20
> > 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.=20
>
> You are probably right, but I wonder if generalizing that way is=20
> going to exceed our experience.  That is, do you think it possible=20
> or reasonable to define the simpler form, get use experience, and=20
> then extend?=20
>

Standardizing something beyond experience -- yes, this would be likely a=20
mistake. However, there are still two ways to proceed. Either standardize=
=20
today today's experience with contract programming, or wait until=20
community's experience grows and standardize it in the future.

My personal impression was that contract programming proposals offered too=
=20
little. Putting aside the interaction with class hierarchies, we get:=20
guaranteed (under certain configuration) automatic runtime checks, and=20
optimizations based on the assumptions that contracts hold. (At lest this=
=20
is my understanding of the proposals.)=20

What I find missing is static checking if contracts are satisfied. You=20
cannot standardize automatic bug detection, but you can make sure that=20
programmers have enough means to convey their intent to static analysers=20
and such. Without such support contract programming features appear=20
incomplete. At least in the sense that certain static transformations are=
=20
performed, but it is not checked if they are safe.

I talked about axioms a lot. I guess I confused two things a particular=20
feature with static analysis support in general.

Regards,
&rzej



--=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_443_6160953.1371194701707
Content-Type: text/html; charset=ISO-8859-2
Content-Transfer-Encoding: quoted-printable

<br><br>W dniu =B6roda, 12 czerwca 2013 05:42:38 UTC+2 u=BFytkownik Lawrenc=
e Crowl napisa=B3:<blockquote class=3D"gmail_quote" style=3D"margin: 0;marg=
in-left: 0.8ex;border-left: 1px #ccc solid;padding-left: 1ex;">On 6/10/13, =
Andrzej Krzemie=F1ski &lt;<a href=3D"javascript:" target=3D"_blank" gdf-obf=
uscated-mailto=3D"dwnaWJWjxo4J">akrz...@gmail.com</a>&gt; wrote:
<br>&gt; It looks to me that axioms are a generalization (or a superset) or
<br>&gt; invariants. Perhaps they should be an integral part of contract
<br>&gt; programming. I wonder what others think.
<br>
<br>You are probably right, but I wonder if generalizing that way is
<br>going to exceed our experience. &nbsp;That is, do you think it possible
<br>or reasonable to define the simpler form, get use experience, and
<br>then extend?
<br></blockquote><div><br>Standardizing something beyond experience -- yes,=
 this would be likely a mistake. However, there are still two ways to proce=
ed. Either standardize today today's experience with contract programming, =
or wait until community's experience grows and standardize it in the future=
..<br><br>My personal impression was that contract programming proposals off=
ered too little. Putting aside the interaction with class hierarchies, we g=
et: guaranteed (under certain configuration) automatic runtime checks, and =
optimizations based on the assumptions that contracts hold. (At lest this i=
s my understanding of the proposals.) <br><br>What I find missing is static=
 checking if contracts are satisfied. You cannot standardize automatic bug =
detection, but you can make sure that programmers have enough means to conv=
ey their intent to static analysers and such. Without such support contract=
 programming features appear incomplete. At least in the sense that certain=
 static transformations are performed, but it is not checked if they are sa=
fe.<br><br>I talked about axioms a lot. I guess I confused two things a par=
ticular feature with static analysis support in general.<br><br>Regards,<br=
>&amp;rzej<br><br><br><br></div>

<p></p>

-- <br />
&nbsp;<br />
--- <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 std-proposals+unsubscribe@isocpp.org.<br />
To post to this group, send email to std-proposals@isocpp.org.<br />
Visit this group at <a href=3D"http://groups.google.com/a/isocpp.org/group/=
std-proposals/">http://groups.google.com/a/isocpp.org/group/std-proposals/<=
/a>.<br />
&nbsp;<br />
&nbsp;<br />

------=_Part_443_6160953.1371194701707--

.

--089e01493cbacc7b0d04df19514b
Content-Type: text/plain; charset=ISO-8859-2
Content-Transfer-Encoding: quoted-printable

While it is true that we may not have enough experience in C++, there are
other languages where we can find experience.

Ada 2012 could be a relevant reference in this area

--
J. Daniel


On Fri, Jun 14, 2013 at 9:25 AM, Andrzej Krzemie=F1ski <akrzemi1@gmail.com>=
wrote:

>
>
> W dniu =B6roda, 12 czerwca 2013 05:42:38 UTC+2 u=BFytkownik Lawrence Crow=
l
> napisa=B3:
>
>> On 6/10/13, Andrzej Krzemie=F1ski <akrz...@gmail.com> wrote:
>> > 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.
>>
>> You are probably right, but I wonder if generalizing that way is
>> going to exceed our experience.  That is, do you think it possible
>> or reasonable to define the simpler form, get use experience, and
>> then extend?
>>
>
> Standardizing something beyond experience -- yes, this would be likely a
> mistake. However, there are still two ways to proceed. Either standardize
> today today's experience with contract programming, or wait until
> community's experience grows and standardize it in the future.
>
> My personal impression was that contract programming proposals offered to=
o
> little. Putting aside the interaction with class hierarchies, we get:
> guaranteed (under certain configuration) automatic runtime checks, and
> optimizations based on the assumptions that contracts hold. (At lest this
> is my understanding of the proposals.)
>
> What I find missing is static checking if contracts are satisfied. You
> cannot standardize automatic bug detection, but you can make sure that
> programmers have enough means to convey their intent to static analysers
> and such. Without such support contract programming features appear
> incomplete. At least in the sense that certain static transformations are
> performed, but it is not checked if they are safe.
>
> I talked about axioms a lot. I guess I confused two things a particular
> feature with static analysis support in general.
>
> 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/.
>
>
>

--=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/.



--089e01493cbacc7b0d04df19514b
Content-Type: text/html; charset=ISO-8859-2
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr">While it is true that we may not have enough experience in=
 C++, there are other languages where we can find experience.<div><br></div=
><div style>Ada 2012 could be a relevant reference in this area</div><div c=
lass=3D"gmail_extra">

<br clear=3D"all"><div><div dir=3D"ltr">--</div></div><div style>J. Daniel<=
/div>
<br><br><div class=3D"gmail_quote">On Fri, Jun 14, 2013 at 9:25 AM, Andrzej=
 Krzemie=F1ski <span dir=3D"ltr">&lt;<a href=3D"mailto:akrzemi1@gmail.com" =
target=3D"_blank">akrzemi1@gmail.com</a>&gt;</span> wrote:<br><blockquote c=
lass=3D"gmail_quote" style=3D"margin:0 0 0 .8ex;border-left:1px #ccc solid;=
padding-left:1ex">

<br><br>W dniu =B6roda, 12 czerwca 2013 05:42:38 UTC+2 u=BFytkownik Lawrenc=
e Crowl napisa=B3:<div class=3D"im"><blockquote class=3D"gmail_quote" style=
=3D"margin:0;margin-left:0.8ex;border-left:1px #ccc solid;padding-left:1ex"=
>On 6/10/13, Andrzej Krzemie=F1ski &lt;<a>akrz...@gmail.com</a>&gt; wrote:
<br>&gt; It looks to me that axioms are a generalization (or a superset) or
<br>&gt; invariants. Perhaps they should be an integral part of contract
<br>&gt; programming. I wonder what others think.
<br>
<br>You are probably right, but I wonder if generalizing that way is
<br>going to exceed our experience. =A0That is, do you think it possible
<br>or reasonable to define the simpler form, get use experience, and
<br>then extend?
<br></blockquote></div><div><br>Standardizing something beyond experience -=
- yes, this would be likely a mistake. However, there are still two ways to=
 proceed. Either standardize today today&#39;s experience with contract pro=
gramming, or wait until community&#39;s experience grows and standardize it=
 in the future.<br>

<br>My personal impression was that contract programming proposals offered =
too little. Putting aside the interaction with class hierarchies, we get: g=
uaranteed (under certain configuration) automatic runtime checks, and optim=
izations based on the assumptions that contracts hold. (At lest this is my =
understanding of the proposals.) <br>

<br>What I find missing is static checking if contracts are satisfied. You =
cannot standardize automatic bug detection, but you can make sure that prog=
rammers have enough means to convey their intent to static analysers and su=
ch. Without such support contract programming features appear incomplete. A=
t least in the sense that certain static transformations are performed, but=
 it is not checked if they are safe.<br>

<br>I talked about axioms a lot. I guess I confused two things a particular=
 feature with static analysis support in general.<br><br>Regards,<br>&amp;r=
zej<br><br><br><br></div><div class=3D"im">

<p></p>

-- <br>
=A0<br>
--- <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%2Bunsubscribe@isocpp.org" target=3D=
"_blank">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">std-proposals@isocpp.org</a>.<br></div>
Visit this group at <a href=3D"http://groups.google.com/a/isocpp.org/group/=
std-proposals/" target=3D"_blank">http://groups.google.com/a/isocpp.org/gro=
up/std-proposals/</a>.<br>
=A0<br>
=A0<br>
</blockquote></div><br></div></div>

<p></p>

-- <br />
&nbsp;<br />
--- <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 std-proposals+unsubscribe@isocpp.org.<br />
To post to this group, send email to std-proposals@isocpp.org.<br />
Visit this group at <a href=3D"http://groups.google.com/a/isocpp.org/group/=
std-proposals/">http://groups.google.com/a/isocpp.org/group/std-proposals/<=
/a>.<br />
&nbsp;<br />
&nbsp;<br />

--089e01493cbacc7b0d04df19514b--

.

Andrzej Krzemie=C5=84ski <akrzemi1@gmail.com> writes:

[...]

| What I find missing is static checking if contracts are satisfied.

How do you propose to check that the second argument to std::find (that
satisfies the requirements of an input iterator) is reachable from the
first argument?  (Preconditions of the std::find algorithm.)

-- Gaby

--=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_18_25114320.1371213659602
Content-Type: text/plain; charset=ISO-8859-2
Content-Transfer-Encoding: quoted-printable



W dniu pi=B1tek, 14 czerwca 2013 11:21:14 UTC+2 u=BFytkownik Gabriel Dos Re=
is=20
napisa=B3:
>
> Andrzej Krzemie=F1ski <akrz...@gmail.com <javascript:>> writes:=20
>
> [...]=20
>
> | What I find missing is static checking if contracts are satisfied.=20
>
> How do you propose to check that the second argument to std::find (that=
=20
> satisfies the requirements of an input iterator) is reachable from the=20
> first argument?  (Preconditions of the std::find algorithm.)=20
>

Do you mean, how static analyser can verify the correctness? It is not of=
=20
course possible to verify it in every case.  I imagine the following=20
definitions would be in place (I use some invented contract syntax):

*  template <typename I>
  bool is_valid_range(I b, I e); *// not defined: just a tag

*  template <typename T>
  axiom vec_range(std::vector<T> v)=20
  {
    is_valid_range(v.begin(), v.end());
  }*

*  template<typename I, typename V> requires ...
  I find(I b, I e, V v)=20
  precondition{ is_valid_range(b, e); }
  postcondition(f) {=20
    is_valid_range(b, f);=20
    is_valid_range(f, e);
    *// ... more*
  }*

Now, if someone writes code:

*  std::vecotr<int> vi =3D {...};
  auto i =3D std::find(vi.begin(), vi.end(), 7);
  auto j =3D std::find(i, vi.end(), 7);*

The first call to *find *can be verified by matching axiom *vec_range* with=
=20
the precondition. The second call can be verified by matching *find*'s=20
postcondition. *is_valid_range *is something like a 'property' or a 'tag'=
=20
that is usually not evaluated. Objects obtain this property and hold it as=
=20
long as no mutable operation is called upon them.

It would still not work though, because *end()* is not *const*, even though=
=20
it doesn't change validity of the property...=20

Regards,
&rzej

--=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_18_25114320.1371213659602
Content-Type: text/html; charset=ISO-8859-2
Content-Transfer-Encoding: quoted-printable

<br><br>W dniu pi=B1tek, 14 czerwca 2013 11:21:14 UTC+2 u=BFytkownik Gabrie=
l Dos Reis napisa=B3:<blockquote class=3D"gmail_quote" style=3D"margin: 0;m=
argin-left: 0.8ex;border-left: 1px #ccc solid;padding-left: 1ex;">Andrzej K=
rzemie=F1ski &lt;<a href=3D"javascript:" target=3D"_blank" gdf-obfuscated-m=
ailto=3D"Y6QlsyovQOYJ">akrz...@gmail.com</a>&gt; writes:
<br>
<br>[...]
<br>
<br>| What I find missing is static checking if contracts are satisfied.
<br>
<br>How do you propose to check that the second argument to std::find (that
<br>satisfies the requirements of an input iterator) is reachable from the
<br>first argument? &nbsp;(Preconditions of the std::find algorithm.)
<br></blockquote><div><br>Do you mean, how static analyser can verify the c=
orrectness? It is not of course possible to verify it in every case.&nbsp; =
I imagine the following definitions would be in place (I use some invented =
contract syntax):<br><br><b>&nbsp; template &lt;typename I&gt;<br>&nbsp; bo=
ol is_valid_range(I b, I e); </b>// not defined: just a tag<br><br><b>&nbsp=
; template &lt;typename T&gt;<br>&nbsp; axiom vec_range(std::vector&lt;T&gt=
; v) <br>&nbsp; {<br>&nbsp;&nbsp; &nbsp;is_valid_range(v.begin(), v.end());=
<br>&nbsp; }</b><br><br><b>&nbsp; template&lt;typename I, typename V&gt; re=
quires ...<br>&nbsp; I find(I b, I e, V v) <br>&nbsp; precondition{ is_vali=
d_range(b, e); }<br>&nbsp; postcondition(f) { <br>&nbsp;&nbsp;&nbsp; is_val=
id_range(b, f); <br>&nbsp;&nbsp;&nbsp; is_valid_range(f, e);<br>&nbsp;&nbsp=
;&nbsp; </b>// ... more<b><br>&nbsp; }</b><br><br>Now, if someone writes co=
de:<br><br><b>&nbsp; std::vecotr&lt;int&gt; vi =3D {...};<br>&nbsp; auto i =
=3D std::find(vi.begin(), vi.end(), 7);<br>&nbsp; auto j =3D std::find(i, v=
i.end(), 7);</b><br><br>The first call to <b>find </b>can be verified by ma=
tching axiom <b>vec_range</b> with the precondition. The second call can be=
 verified by matching <b>find</b>'s postcondition. <b>is_valid_range </b>is=
 something like a 'property' or a 'tag' that is usually not evaluated. Obje=
cts obtain this property and hold it as long as no mutable operation is cal=
led upon them.<br><br>It would still not work though, because <b>end()</b> =
is not <b>const</b>, even though it doesn't change validity of the property=
.... <br><br>Regards,<br>&amp;rzej<br></div>

<p></p>

-- <br />
&nbsp;<br />
--- <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 std-proposals+unsubscribe@isocpp.org.<br />
To post to this group, send email to std-proposals@isocpp.org.<br />
Visit this group at <a href=3D"http://groups.google.com/a/isocpp.org/group/=
std-proposals/">http://groups.google.com/a/isocpp.org/group/std-proposals/<=
/a>.<br />
&nbsp;<br />
&nbsp;<br />

------=_Part_18_25114320.1371213659602--

.

Andrzej Krzemie=F1ski <akrzemi1@gmail.com> writes:

| W dniu pi=B1tek, 14 czerwca 2013 11:21:14 UTC+2 u=BFytkownik Gabriel Dos =
Reis
| napisa=B3:
|=20
|     Andrzej Krzemie=F1ski <akrz...@gmail.com> writes:
|=20
|     [...]
|=20
|     | What I find missing is static checking if contracts are satisfied.
|=20
|     How do you propose to check that the second argument to std::find (th=
at
|     satisfies the requirements of an input iterator) is reachable from th=
e
|     first argument?  (Preconditions of the std::find algorithm.)
|=20
|=20
| Do you mean, how static analyser can verify the correctness? It is not of
| course possible to verify it in every case.  I imagine the following
| definitions would be in place (I use some invented contract syntax):
|=20
|   template <typename I>
|   bool is_valid_range(I b, I e); // not defined: just a tag
|=20
|   template <typename T>
|   axiom vec_range(std::vector<T> v)
|   {
|     is_valid_range(v.begin(), v.end());
|   }
|=20
|   template<typename I, typename V> requires ...
|   I find(I b, I e, V v)
|   precondition{ is_valid_range(b, e); }
|   postcondition(f) {
|     is_valid_range(b, f);
|     is_valid_range(f, e);
|     // ... more
|   }

One property of input iterators is that once copied, the original can't
be used again.  Also, I am not sure what the purpose of is_valid_range()
is; the comment says it isn't defined.

-- Gaby

--=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/.



.

On 6/14/13, Andrzej Krzemie=F1ski <akrzemi1@gmail.com> wrote:
> My personal impression was that contract programming proposals
> offered too little. Putting aside the interaction with class
> hierarchies, we get: guaranteed (under certain configuration)
> automatic runtime checks, and optimizations based on the
> assumptions that contracts hold. (At lest this is my understanding
> of the proposals.)
>
> What I find missing is static checking if contracts are
> satisfied. You cannot standardize automatic bug detection, but
> you can make sure that programmers have enough means to convey
> their intent to static analysers and such. Without such support
> contract programming features appear incomplete. At least in the
> sense that certain static transformations are performed, but it
> is not checked if they are safe.

I don't see why the ability to do static checking of contracts does
not fall out of pretty much any contract proposal.  Consider

type* producer();
void consumer(type* arg) preconditon { arg !=3D NULL };
.....; consumer(producer()); ....

The compiler that the postcondition of the call to producer is
insufficient to satisfy the precondition of the call to the consumer.
A tool can can warn in this case.

On the other hand, in

type* producer() postcondition { result !=3D NULL; };
void consumer(type* arg) preconditon { arg !=3D NULL; };
.....; consumer(producer()); ....

the postcondition easily satisfies the precondition.  The compiler
can avoid generating the precondition check based on that
satisfiability.

Compilers are not going to be able to always prove that functions
preconditions are satisfied.  Indeed, I expect some preconditions
would be hard to specify in code, and so would be out of reach of
any automation.  So, I don't know what we could normatively say
about static checking of interfaces.  We can provide the data,
and hope tool writers do good things with it.
I think they will because in the second case above,
a warning would encourage the programmer to either make
the postcondition more complete or add an explicit check.

I think analyses that complement the cases were the compiler
exploits undefined behavior would be particularly valuable.
For example, in

int load(int* p) { return *p; }

loading through a null pointer is undefined behavior, so a tool
could infer a missing precondition and warn the programmer that
the function precondition is incomplete.

int load(int* p) precondition { p !=3D NULL; } { return *p; }

Adding that precondition means that calls to load are now amenable
to analysis.

--=20
Lawrence Crowl

--=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/.



.

On 6/14/13, Gabriel Dos Reis <gdr@axiomatics.org> wrote:
> Andrzej Krzemie=F1ski <akrzemi1@gmail.com> writes:
> > 14 czerwca 2013 Gabriel Dos Reis:
> > > Andrzej Krzemie=F1ski <akrz...@gmail.com> writes:
> > > > What I find missing is static checking if contracts are
> > > > satisfied.
> > >
> > > How do you propose to check that the second argument
> > > to std::find (that satisfies the requirements of an
> > > input iterator) is reachable from the first argument?
> > > (Preconditions of the std::find algorithm.)
> >
> > Do you mean, how static analyser can verify the correctness? It
> > is not of course possible to verify it in every case.  I imagine
> > the following definitions would be in place (I use some invented
> > contract syntax):
> >
> >   template <typename I>
> >   bool is_valid_range(I b, I e); // not defined: just a tag
> >
> >   template <typename T>
> >   axiom vec_range(std::vector<T> v)
> >   {
> >     is_valid_range(v.begin(), v.end());
> >   }
> >
> >   template<typename I, typename V> requires ...
> >   I find(I b, I e, V v)
> >   precondition{ is_valid_range(b, e); }
> >   postcondition(f) {
> >     is_valid_range(b, f);
> >     is_valid_range(f, e);
> >     // ... more
> >   }
>
> One property of input iterators is that once copied, the original
> can't be used again.  Also, I am not sure what the purpose of
> is_valid_range() is; the comment says it isn't defined.

We could probably check this with type state, but certainly the
earlier contract programming proposals do not have mechanisms
for that.

--=20
Lawrence Crowl

--=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/.



.

Lawrence Crowl <crowl@googlers.com> writes:

[...]

| I think analyses that complement the cases were the compiler
| exploits undefined behavior would be particularly valuable.

In the scope of C++, I think this is probably the most compeling case
for "programming by contract."

-- Gaby

--

---
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/.



.

Lawrence Crowl <crowl@googlers.com> writes:

| On 6/14/13, Gabriel Dos Reis <gdr@axiomatics.org> wrote:
| > Andrzej Krzemie=F1ski <akrzemi1@gmail.com> writes:
| > > 14 czerwca 2013 Gabriel Dos Reis:
| > > > Andrzej Krzemie=F1ski <akrz...@gmail.com> writes:
| > > > > What I find missing is static checking if contracts are
| > > > > satisfied.
| > > >
| > > > How do you propose to check that the second argument
| > > > to std::find (that satisfies the requirements of an
| > > > input iterator) is reachable from the first argument?
| > > > (Preconditions of the std::find algorithm.)
| > >
| > > Do you mean, how static analyser can verify the correctness? It
| > > is not of course possible to verify it in every case.  I imagine
| > > the following definitions would be in place (I use some invented
| > > contract syntax):
| > >
| > >   template <typename I>
| > >   bool is_valid_range(I b, I e); // not defined: just a tag
| > >
| > >   template <typename T>
| > >   axiom vec_range(std::vector<T> v)
| > >   {
| > >     is_valid_range(v.begin(), v.end());
| > >   }
| > >
| > >   template<typename I, typename V> requires ...
| > >   I find(I b, I e, V v)
| > >   precondition{ is_valid_range(b, e); }
| > >   postcondition(f) {
| > >     is_valid_range(b, f);
| > >     is_valid_range(f, e);
| > >     // ... more
| > >   }
| >
| > One property of input iterators is that once copied, the original
| > can't be used again.  Also, I am not sure what the purpose of
| > is_valid_range() is; the comment says it isn't defined.
|=20
| We could probably check this with type state, but certainly the
| earlier contract programming proposals do not have mechanisms
| for that.

and assuming we know how to model the concept of input iterators
adequately... =20

-- Gaby

--=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_39_150202.1371456624035
Content-Type: text/plain; charset=ISO-8859-2
Content-Transfer-Encoding: quoted-printable



W dniu pi=B1tek, 14 czerwca 2013 17:34:56 UTC+2 u=BFytkownik Gabriel Dos Re=
is=20
napisa=B3:
>
> Andrzej Krzemie=F1ski <akrz...@gmail.com <javascript:>> writes:=20
>
> | W dniu pi=B1tek, 14 czerwca 2013 11:21:14 UTC+2 u=BFytkownik Gabriel Do=
s=20
> Reis=20
> | napisa=B3:=20
> |=20
> |     Andrzej Krzemie=F1ski <akrz...@gmail.com> writes:=20
> |=20
> |     [...]=20
> |=20
> |     | What I find missing is static checking if contracts are satisfied=
..=20
> |=20
> |     How do you propose to check that the second argument to std::find=
=20
> (that=20
> |     satisfies the requirements of an input iterator) is reachable from=
=20
> the=20
> |     first argument?  (Preconditions of the std::find algorithm.)=20
> |=20
> |=20
> | Do you mean, how static analyser can verify the correctness? It is not=
=20
> of=20
> | course possible to verify it in every case.  I imagine the following=20
> | definitions would be in place (I use some invented contract syntax):=20
> |=20
> |   template <typename I>=20
> |   bool is_valid_range(I b, I e); // not defined: just a tag=20
> |=20
> |   template <typename T>=20
> |   axiom vec_range(std::vector<T> v)=20
> |   {=20
> |     is_valid_range(v.begin(), v.end());=20
> |   }=20
> |=20
> |   template<typename I, typename V> requires ...=20
> |   I find(I b, I e, V v)=20
> |   precondition{ is_valid_range(b, e); }=20
> |   postcondition(f) {=20
> |     is_valid_range(b, f);=20
> |     is_valid_range(f, e);=20
> |     // ... more=20
> |   }=20
>
> One property of input iterators is that once copied, the original can't=
=20
> be used again.  Also, I am not sure what the purpose of is_valid_range()=
=20
> is; the comment says it isn't defined.=20
>

Really? I used to think that it is operation *it++ that invalidates the=20
copies of the input iterator, not the copying itself. Also, your example is=
=20
tricky because it tests a couple of difficulties at the same time:

   - A predicate that cannot be formed
   - A predicate that has side effects when it is evaluated
   - A predicate on two arguments that are created separately from one=20
   another
   - A predicate on non-value semantic types (we use iterators as=20
   references to remote objects/memory)

so, let me only address the first bullet here, by using a simpler example:

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

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

And imagine that for some reason *is_initialized *cannot be formed/define.=
=20
This *is_initialized* would be used by static analyser not as a function,=
=20
which can be evaluated, but as a "tag" or a "label". Objects at certain=20
points in time acquire the label, keep it for certain time, and then, they=
=20
can loose it as an effect of a mutable operation.
void fun( optional<T> & o )
{
  // property is_initialized(o) cannot be determined
  o =3D T{1};
  // is_initialized(o) holds, even though we do not know what it means
  *o; // precondition is met
  mutable_fun(o);
  // property is_initialized(o) cann no longer be determined to hold
}


Regards,
&rzej

*
*

--=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_39_150202.1371456624035
Content-Type: text/html; charset=ISO-8859-2
Content-Transfer-Encoding: quoted-printable

<br><br>W dniu pi=B1tek, 14 czerwca 2013 17:34:56 UTC+2 u=BFytkownik Gabrie=
l Dos Reis napisa=B3:<blockquote class=3D"gmail_quote" style=3D"margin: 0;m=
argin-left: 0.8ex;border-left: 1px #ccc solid;padding-left: 1ex;">Andrzej K=
rzemie=F1ski &lt;<a href=3D"javascript:" target=3D"_blank" gdf-obfuscated-m=
ailto=3D"YXXxD6hsoEkJ">akrz...@gmail.com</a>&gt; writes:
<br>
<br>| W dniu pi=B1tek, 14 czerwca 2013 11:21:14 UTC+2 u=BFytkownik Gabriel =
Dos Reis
<br>| napisa=B3:
<br>|=20
<br>| &nbsp; &nbsp; Andrzej Krzemie=F1ski &lt;<a>akrz...@gmail.com</a>&gt; =
writes:
<br>|=20
<br>| &nbsp; &nbsp; [...]
<br>|=20
<br>| &nbsp; &nbsp; | What I find missing is static checking if contracts a=
re satisfied.
<br>|=20
<br>| &nbsp; &nbsp; How do you propose to check that the second argument to=
 std::find (that
<br>| &nbsp; &nbsp; satisfies the requirements of an input iterator) is rea=
chable from the
<br>| &nbsp; &nbsp; first argument? &nbsp;(Preconditions of the std::find a=
lgorithm.)
<br>|=20
<br>|=20
<br>| Do you mean, how static analyser can verify the correctness? It is no=
t of
<br>| course possible to verify it in every case. &nbsp;I imagine the follo=
wing
<br>| definitions would be in place (I use some invented contract syntax):
<br>|=20
<br>| &nbsp; template &lt;typename I&gt;
<br>| &nbsp; bool is_valid_range(I b, I e); // not defined: just a tag
<br>|=20
<br>| &nbsp; template &lt;typename T&gt;
<br>| &nbsp; axiom vec_range(std::vector&lt;T&gt; v)
<br>| &nbsp; {
<br>| &nbsp; &nbsp; is_valid_range(v.begin(), v.end());
<br>| &nbsp; }
<br>|=20
<br>| &nbsp; template&lt;typename I, typename V&gt; requires ...
<br>| &nbsp; I find(I b, I e, V v)
<br>| &nbsp; precondition{ is_valid_range(b, e); }
<br>| &nbsp; postcondition(f) {
<br>| &nbsp; &nbsp; is_valid_range(b, f);
<br>| &nbsp; &nbsp; is_valid_range(f, e);
<br>| &nbsp; &nbsp; // ... more
<br>| &nbsp; }
<br>
<br>One property of input iterators is that once copied, the original can't
<br>be used again. &nbsp;Also, I am not sure what the purpose of is_valid_r=
ange()
<br>is; the comment says it isn't defined.
<br></blockquote><div><br>Really? I used to think that it is operation <spa=
n style=3D"font-family: courier new,monospace;">*it++</span> that invalidat=
es the copies of the input iterator, not the copying itself. Also, your exa=
mple is tricky because it tests a couple of difficulties at the same time:<=
br><ul><li>A predicate that cannot be formed</li><li>A predicate that has s=
ide effects when it is evaluated</li><li>A predicate on two arguments that =
are created separately from one another</li><li>A predicate on non-value se=
mantic types (we use iterators as references to remote objects/memory)</li>=
</ul><p>so, let me only address the first bullet here, by using a simpler e=
xample:</p><p style=3D"margin-left: 40px;"><b>T&amp; optional&lt;T&gt;::ope=
rator*()<br>precondition{ is_initialized(*this) };<br><br>T&amp; optional&l=
t;T&gt;::operator=3D(T&amp;&amp;)<br>postcondition{ </b><b><b>is_initialize=
d</b>(*this) }; <br></b></p><p>And imagine that for some reason <b>is_initi=
alized </b>cannot be formed/define. This <b>is_initialized</b> would be use=
d by static analyser not as a function, which can be evaluated, but as a "t=
ag" or a "label". Objects at certain points in time acquire the label, keep=
 it for certain time, and then, they can loose it as an effect of a mutable=
 operation.</p><div class=3D"prettyprint" style=3D"background-color: rgb(25=
0, 250, 250); border-color: rgb(187, 187, 187); border-style: solid; border=
-width: 1px; word-wrap: break-word;"><code class=3D"prettyprint"><div class=
=3D"subprettyprint"><code class=3D"prettyprint"><span style=3D"color: #008;=
" class=3D"styled-by-prettify">void</span><span style=3D"color: #000;" clas=
s=3D"styled-by-prettify"> fun</span><span style=3D"color: #660;" class=3D"s=
tyled-by-prettify">(</span><span style=3D"color: #000;" class=3D"styled-by-=
prettify"> optional</span><span style=3D"color: #660;" class=3D"styled-by-p=
rettify">&lt;</span><span style=3D"color: #000;" class=3D"styled-by-prettif=
y">T</span><span style=3D"color: #660;" class=3D"styled-by-prettify">&gt;</=
span><span style=3D"color: #000;" class=3D"styled-by-prettify"> </span><spa=
n style=3D"color: #660;" class=3D"styled-by-prettify">&amp;</span><span sty=
le=3D"color: #000;" class=3D"styled-by-prettify"> o </span><span style=3D"c=
olor: #660;" class=3D"styled-by-prettify">)</span><span style=3D"color: #00=
0;" class=3D"styled-by-prettify"><br>{<br>&nbsp; // property is_initialized=
(o) cannot be determined<br>&nbsp; o =3D T{1};<br>&nbsp; // is_initialized(=
o) holds, even though we do not know what it means<br>&nbsp; *o; // precond=
ition is met<br>&nbsp; mutable_fun(o);<br>&nbsp; // property is_initialized=
(o) cann no longer be determined to hold<br>}<br></span></code><span style=
=3D"color: #660;" class=3D"styled-by-prettify"></span></div></code></div><b=
r><br><p>Regards,<br>&amp;rzej<br></p><p><b><br></b></p></div>

<p></p>

-- <br />
&nbsp;<br />
--- <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 std-proposals+unsubscribe@isocpp.org.<br />
To post to this group, send email to std-proposals@isocpp.org.<br />
Visit this group at <a href=3D"http://groups.google.com/a/isocpp.org/group/=
std-proposals/">http://groups.google.com/a/isocpp.org/group/std-proposals/<=
/a>.<br />
&nbsp;<br />
&nbsp;<br />

------=_Part_39_150202.1371456624035--

.

------=_Part_1488_18528662.1371538679755
Content-Type: text/plain; charset=ISO-8859-2
Content-Transfer-Encoding: quoted-printable



W dniu poniedzia=B3ek, 17 czerwca 2013 01:40:45 UTC+2 u=BFytkownik Lawrence=
=20
Crowl napisa=B3:
>
> On 6/14/13, Andrzej Krzemie=F1ski <akrz...@gmail.com <javascript:>> wrote=
:=20
> > My personal impression was that contract programming proposals=20
> > offered too little. Putting aside the interaction with class=20
> > hierarchies, we get: guaranteed (under certain configuration)=20
> > automatic runtime checks, and optimizations based on the=20
> > assumptions that contracts hold. (At lest this is my understanding=20
> > of the proposals.)=20
> >=20
> > What I find missing is static checking if contracts are=20
> > satisfied. You cannot standardize automatic bug detection, but=20
> > you can make sure that programmers have enough means to convey=20
> > their intent to static analysers and such. Without such support=20
> > contract programming features appear incomplete. At least in the=20
> > sense that certain static transformations are performed, but it=20
> > is not checked if they are safe.=20
>
> I don't see why the ability to do static checking of contracts does=20
> not fall out of pretty much any contract proposal.  Consider=20
>
> type* producer();=20
> void consumer(type* arg) preconditon { arg !=3D NULL };=20
> ....; consumer(producer()); ....=20
>
> The compiler that the postcondition of the call to producer is=20
> insufficient to satisfy the precondition of the call to the consumer.=20
> A tool can can warn in this case.=20
>
> On the other hand, in=20
>
> type* producer() postcondition { result !=3D NULL; };=20
> void consumer(type* arg) preconditon { arg !=3D NULL; };=20
> ....; consumer(producer()); ....=20
>
> the postcondition easily satisfies the precondition.  The compiler=20
> can avoid generating the precondition check based on that=20
> satisfiability.=20
>

True, if one function's postcondition is _exactly_ same as other function's=
=20
precondition, then static analyser can exploit this in any contract=20
programming framework. The situation is different when preconditions and=20
postconditions cannot be matched exactly. For instance, one function=20
ensures property *is_positive(e)* and another requires property *
is_nonnegative(e)*. The former implies the latter, but the analyser would=
=20
not know it. Similarly, there could be more than one way of stating the=20
same state. In case of pointer, it is *bool(p)* and *p !=3D nullptr*. Becau=
se=20
pointers are built into the language compilers/analysers can understand the=
=20
"redundancy" in the interface, but in similar case of *std::optional*,=20
automated tools will not know that* bool(o) *is equivalent to* o !=3D nullo=
pt*.=20
My personal opinion is that this element would be really missing from a=20
"toolset" for enhancing static analysis. And on the other hand a construct=
=20
for expressing such relationships has already been devised. Whether this=20
ability is essential or not for the first "pass" of contract programming=20
enhancements is I guess very subjective.=20
=20

>
> Compilers are not going to be able to always prove that functions=20
> preconditions are satisfied.  Indeed, I expect some preconditions=20
> would be hard to specify in code, and so would be out of reach of=20
> any automation.  So, I don't know what we could normatively say=20
> about static checking of interfaces. =20


The standard could define the violation of the contract as undefined=20
behaviour. This opens the way for contract based optimizations and=20
instrumentation. And this is already so for cases like *
vector<T>::operator[]*.
=20

> We can provide the data,=20
> and hope tool writers do good things with it.=20
> I think they will because in the second case above,=20
> a warning would encourage the programmer to either make=20
> the postcondition more complete or add an explicit check.=20
>
> I think analyses that complement the cases were the compiler=20
> exploits undefined behavior would be particularly valuable.=20
> For example, in=20
>
> int load(int* p) { return *p; }=20
>
> loading through a null pointer is undefined behavior, so a tool=20
> could infer a missing precondition and warn the programmer that=20
> the function precondition is incomplete.=20
>
> int load(int* p) precondition { p !=3D NULL; } { return *p; }=20
>
> Adding that precondition means that calls to load are now amenable=20
> to analysis.=20
>
> --=20
> Lawrence Crowl=20
>

--=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_1488_18528662.1371538679755
Content-Type: text/html; charset=ISO-8859-2
Content-Transfer-Encoding: quoted-printable

<br><br>W dniu poniedzia=B3ek, 17 czerwca 2013 01:40:45 UTC+2 u=BFytkownik =
Lawrence Crowl napisa=B3:<blockquote class=3D"gmail_quote" style=3D"margin:=
 0;margin-left: 0.8ex;border-left: 1px #ccc solid;padding-left: 1ex;">On 6/=
14/13, Andrzej Krzemie=F1ski &lt;<a href=3D"javascript:" target=3D"_blank" =
gdf-obfuscated-mailto=3D"LjZLenHSIXUJ">akrz...@gmail.com</a>&gt; wrote:
<br>&gt; My personal impression was that contract programming proposals
<br>&gt; offered too little. Putting aside the interaction with class
<br>&gt; hierarchies, we get: guaranteed (under certain configuration)
<br>&gt; automatic runtime checks, and optimizations based on the
<br>&gt; assumptions that contracts hold. (At lest this is my understanding
<br>&gt; of the proposals.)
<br>&gt;
<br>&gt; What I find missing is static checking if contracts are
<br>&gt; satisfied. You cannot standardize automatic bug detection, but
<br>&gt; you can make sure that programmers have enough means to convey
<br>&gt; their intent to static analysers and such. Without such support
<br>&gt; contract programming features appear incomplete. At least in the
<br>&gt; sense that certain static transformations are performed, but it
<br>&gt; is not checked if they are safe.
<br>
<br>I don't see why the ability to do static checking of contracts does
<br>not fall out of pretty much any contract proposal. &nbsp;Consider
<br>
<br>type* producer();
<br>void consumer(type* arg) preconditon { arg !=3D NULL };
<br>....; consumer(producer()); ....
<br>
<br>The compiler that the postcondition of the call to producer is
<br>insufficient to satisfy the precondition of the call to the consumer.
<br>A tool can can warn in this case.
<br>
<br>On the other hand, in
<br>
<br>type* producer() postcondition { result !=3D NULL; };
<br>void consumer(type* arg) preconditon { arg !=3D NULL; };
<br>....; consumer(producer()); ....
<br>
<br>the postcondition easily satisfies the precondition. &nbsp;The compiler
<br>can avoid generating the precondition check based on that
<br>satisfiability.
<br></blockquote><div><br>True, if one function's postcondition is _exactly=
_ same as other function's precondition, then static analyser can exploit t=
his in any contract programming framework. The situation is different when =
preconditions and postconditions cannot be matched exactly. For instance, o=
ne function ensures property <b>is_positive(e)</b> and another requires pro=
perty <b>is_nonnegative(e)</b>. The former implies the latter, but the anal=
yser would not know it. Similarly, there could be more than one way of stat=
ing the same state. In case of pointer, it is <b>bool(p)</b> and <b>p !=3D =
nullptr</b>. Because pointers are built into the language compilers/analyse=
rs can understand the "redundancy" in the interface, but in similar case of=
 <b>std::optional</b>, automated tools will not know that<b> bool(o) </b>is=
 equivalent to<b> o !=3D nullopt</b>. My personal opinion is that this elem=
ent would be really missing from a "toolset" for enhancing static analysis.=
 And on the other hand a construct for expressing such relationships has al=
ready been devised. Whether this ability is essential or not for the first =
"pass" of contract programming enhancements is I guess very subjective. <br=
>&nbsp;<br></div><blockquote class=3D"gmail_quote" style=3D"margin: 0;margi=
n-left: 0.8ex;border-left: 1px #ccc solid;padding-left: 1ex;">
<br>Compilers are not going to be able to always prove that functions
<br>preconditions are satisfied. &nbsp;Indeed, I expect some preconditions
<br>would be hard to specify in code, and so would be out of reach of
<br>any automation. &nbsp;So, I don't know what we could normatively say
<br>about static checking of interfaces. &nbsp;</blockquote><div><br>The st=
andard could define the violation of the contract as undefined behaviour. T=
his opens the way for contract based optimizations and instrumentation. And=
 this is already so for cases like <b>vector&lt;T&gt;::operator[]</b>.<br>&=
nbsp;</div><blockquote class=3D"gmail_quote" style=3D"margin: 0;margin-left=
: 0.8ex;border-left: 1px #ccc solid;padding-left: 1ex;">We can provide the =
data,
<br>and hope tool writers do good things with it.
<br>I think they will because in the second case above,
<br>a warning would encourage the programmer to either make
<br>the postcondition more complete or add an explicit check.
<br>
<br>I think analyses that complement the cases were the compiler
<br>exploits undefined behavior would be particularly valuable.
<br>For example, in
<br>
<br>int load(int* p) { return *p; }
<br>
<br>loading through a null pointer is undefined behavior, so a tool
<br>could infer a missing precondition and warn the programmer that
<br>the function precondition is incomplete.
<br>
<br>int load(int* p) precondition { p !=3D NULL; } { return *p; }
<br>
<br>Adding that precondition means that calls to load are now amenable
<br>to analysis.
<br>
<br>--=20
<br>Lawrence Crowl
<br></blockquote>

<p></p>

-- <br />
&nbsp;<br />
--- <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 std-proposals+unsubscribe@isocpp.org.<br />
To post to this group, send email to std-proposals@isocpp.org.<br />
Visit this group at <a href=3D"http://groups.google.com/a/isocpp.org/group/=
std-proposals/">http://groups.google.com/a/isocpp.org/group/std-proposals/<=
/a>.<br />
&nbsp;<br />
&nbsp;<br />

------=_Part_1488_18528662.1371538679755--

.

On 6/17/13, Andrzej Krzemie=F1ski <akrzemi1@gmail.com> wrote:
> 17 czerwca 2013 Lawrence Crowl napisa=B3:
> > On 6/14/13, Andrzej Krzemie=F1ski wrote:
> > > My personal impression was that contract programming
> > > proposals offered too little. Putting aside the interaction
> > > with class hierarchies, we get: guaranteed (under certain
> > > configuration) automatic runtime checks, and optimizations
> > > based on the assumptions that contracts hold. (At lest this
> > > is my understanding of the proposals.)
> > >
> > > What I find missing is static checking if contracts are
> > > satisfied. You cannot standardize automatic bug detection,
> > > but you can make sure that programmers have enough means to
> > > convey their intent to static analysers and such. Without such
> > > support contract programming features appear incomplete. At
> > > least in the sense that certain static transformations are
> > > performed, but it is not checked if they are safe.
> >
> > I don't see why the ability to do static checking of contracts
> > does not fall out of pretty much any contract proposal.  Consider
> >
> > type* producer();
> > void consumer(type* arg) preconditon { arg !=3D NULL };
> > ....; consumer(producer()); ....
> >
> > The compiler that the postcondition of the call to producer
> > is insufficient to satisfy the precondition of the call to
> > the consumer.  A tool can can warn in this case.
> >
> > On the other hand, in
> >
> > type* producer() postcondition { result !=3D NULL; };
> > void consumer(type* arg) preconditon { arg !=3D NULL; };
> > ....; consumer(producer()); ....
> >
> > the postcondition easily satisfies the precondition.  The
> > compiler can avoid generating the precondition check based on
> > that satisfiability.
>
> True, if one function's postcondition is _exactly_ same as other
> function's precondition, then static analyser can exploit this in
> any contract programming framework. The situation is different when
> preconditions and postconditions cannot be matched exactly. For
> instance, one function ensures property *is_positive(e)*
> and another requires property * is_nonnegative(e)*. The former
> implies the latter, but the analyser would not know it.

If is_positive(e) and is_nonnegative(e) are inline functions
implemented as e>0 and e>=3D0, then the compiler certainly can make the
proper inferences.  In any case, the compiler can only manipulate
predicates that are within its algebraic domain, and so it would
be best if preconditions were written to a reasonable domain.

> Similarly, there could be more than one way of stating the
> same state. In case of pointer, it is *bool(p)* and *p !=3D
> nullptr*. Because pointers are built into the language
> compilers/analysers can understand the "redundancy" in the
> interface, but in similar case of *std::optional*, automated
> tools will not know that* bool(o) *is equivalent to* o !=3D nullopt*.

But if the postcondition on bool(o) is result =3D=3D (o!=3Dnullopt),
then that interpretation is within reach.  It will take work to
specify preconditions and postconditions in a manner that is both
useful to compilers and to programmers.

> My personal opinion is that this element would be really missing
> from a "toolset" for enhancing static analysis. And on the other
> hand a construct for expressing such relationships has already
> been devised. Whether this ability is essential or not for the
> first "pass" of contract programming enhancements is I guess
> very subjective.

I am not sure that we are all that far from what you suggest, at
least for a reasonable subset of the preconditions.  Can you write
a paper describing what you want in detail?

> > Compilers are not going to be able to always prove that functions
> > preconditions are satisfied.  Indeed, I expect some preconditions
> > would be hard to specify in code, and so would be out of reach
> > of any automation.  So, I don't know what we could normatively
> > say about static checking of interfaces.
>
> The standard could define the violation of the contract as
> undefined behaviour. This opens the way for contract based
> optimizations and instrumentation. And this is already so for
> cases like * vector<T>::operator[]*.

The prior proposals did define violation as undefined behavior.

> > We can provide the data, and hope tool writers do good things
> > with it.  I think they will because in the second case above,
> > a warning would encourage the programmer to either make the
> > postcondition more complete or add an explicit check.
> >
> > I think analyses that complement the cases were the compiler
> > exploits undefined behavior would be particularly valuable.
> > For example, in
> >
> > int load(int* p) { return *p; }
> >
> > loading through a null pointer is undefined behavior, so a tool
> > could infer a missing precondition and warn the programmer that
> > the function precondition is incomplete.
> >
> > int load(int* p) precondition { p !=3D NULL; } { return *p; }
> >
> > Adding that precondition means that calls to load are now
> > amenable to analysis.

--=20
Lawrence Crowl

--=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_10_11299482.1404897813754
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: quoted-printable



W dniu wtorek, 18 czerwca 2013 20:54:53 UTC+2 u=C5=BCytkownik Lawrence Crow=
l=20
napisa=C5=82:
>
> On 6/17/13, Andrzej Krzemie=C5=84ski <akrz...@gmail.com <javascript:>> wr=
ote:=20
> > 17 czerwca 2013 Lawrence Crowl napisa=C5=82:=20
> > > On 6/14/13, Andrzej Krzemie=C5=84ski wrote:=20
> > > > My personal impression was that contract programming=20
> > > > proposals offered too little. Putting aside the interaction=20
> > > > with class hierarchies, we get: guaranteed (under certain=20
> > > > configuration) automatic runtime checks, and optimizations=20
> > > > based on the assumptions that contracts hold. (At lest this=20
> > > > is my understanding of the proposals.)=20
> > > >=20
> > > > What I find missing is static checking if contracts are=20
> > > > satisfied. You cannot standardize automatic bug detection,=20
> > > > but you can make sure that programmers have enough means to=20
> > > > convey their intent to static analysers and such. Without such=20
> > > > support contract programming features appear incomplete. At=20
> > > > least in the sense that certain static transformations are=20
> > > > performed, but it is not checked if they are safe.=20
> > >=20
> > > I don't see why the ability to do static checking of contracts=20
> > > does not fall out of pretty much any contract proposal.  Consider=20
> > >=20
> > > type* producer();=20
> > > void consumer(type* arg) preconditon { arg !=3D NULL };=20
> > > ....; consumer(producer()); ....=20
> > >=20
> > > The compiler that the postcondition of the call to producer=20
> > > is insufficient to satisfy the precondition of the call to=20
> > > the consumer.  A tool can can warn in this case.=20
> > >=20
> > > On the other hand, in=20
> > >=20
> > > type* producer() postcondition { result !=3D NULL; };=20
> > > void consumer(type* arg) preconditon { arg !=3D NULL; };=20
> > > ....; consumer(producer()); ....=20
> > >=20
> > > the postcondition easily satisfies the precondition.  The=20
> > > compiler can avoid generating the precondition check based on=20
> > > that satisfiability.=20
> >=20
> > True, if one function's postcondition is _exactly_ same as other=20
> > function's precondition, then static analyser can exploit this in=20
> > any contract programming framework. The situation is different when=20
> > preconditions and postconditions cannot be matched exactly. For=20
> > instance, one function ensures property *is_positive(e)*=20
> > and another requires property * is_nonnegative(e)*. The former=20
> > implies the latter, but the analyser would not know it.=20
>
> If is_positive(e) and is_nonnegative(e) are inline functions=20
> implemented as e>0 and e>=3D0, then the compiler certainly can make the=
=20
> proper inferences.  In any case, the compiler can only manipulate=20
> predicates that are within its algebraic domain, and so it would=20
> be best if preconditions were written to a reasonable domain.=20
>
> > Similarly, there could be more than one way of stating the=20
> > same state. In case of pointer, it is *bool(p)* and *p !=3D=20
> > nullptr*. Because pointers are built into the language=20
> > compilers/analysers can understand the "redundancy" in the=20
> > interface, but in similar case of *std::optional*, automated=20
> > tools will not know that* bool(o) *is equivalent to* o !=3D nullopt*.=
=20
>
> But if the postcondition on bool(o) is result =3D=3D (o!=3Dnullopt),=20
> then that interpretation is within reach.  It will take work to=20
> specify preconditions and postconditions in a manner that is both=20
> useful to compilers and to programmers.=20
>
> > My personal opinion is that this element would be really missing=20
> > from a "toolset" for enhancing static analysis. And on the other=20
> > hand a construct for expressing such relationships has already=20
> > been devised. Whether this ability is essential or not for the=20
> > first "pass" of contract programming enhancements is I guess=20
> > very subjective.=20
>
> I am not sure that we are all that far from what you suggest, at=20
> least for a reasonable subset of the preconditions.  Can you write=20
> a paper describing what you want in detail?=20
>

I describe some examples of what I mean in the following draft paper:
http://htmlpreview.github.io/?https://github.com/akrzemi1/contract/blob/mas=
ter/contract.html=20

Regards,
&rzej

--=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_10_11299482.1404897813754
Content-Type: text/html; charset=UTF-8
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr"><br><br>W dniu wtorek, 18 czerwca 2013 20:54:53 UTC+2 u=C5=
=BCytkownik Lawrence Crowl napisa=C5=82:<blockquote class=3D"gmail_quote" s=
tyle=3D"margin: 0;margin-left: 0.8ex;border-left: 1px #ccc solid;padding-le=
ft: 1ex;">On 6/17/13, Andrzej Krzemie=C5=84ski &lt;<a href=3D"javascript:" =
target=3D"_blank" gdf-obfuscated-mailto=3D"ogedC7E4sGIJ" onmousedown=3D"thi=
s.href=3D'javascript:';return true;" onclick=3D"this.href=3D'javascript:';r=
eturn true;">akrz...@gmail.com</a>&gt; wrote:
<br>&gt; 17 czerwca 2013 Lawrence Crowl napisa=C5=82:
<br>&gt; &gt; On 6/14/13, Andrzej Krzemie=C5=84ski wrote:
<br>&gt; &gt; &gt; My personal impression was that contract programming
<br>&gt; &gt; &gt; proposals offered too little. Putting aside the interact=
ion
<br>&gt; &gt; &gt; with class hierarchies, we get: guaranteed (under certai=
n
<br>&gt; &gt; &gt; configuration) automatic runtime checks, and optimizatio=
ns
<br>&gt; &gt; &gt; based on the assumptions that contracts hold. (At lest t=
his
<br>&gt; &gt; &gt; is my understanding of the proposals.)
<br>&gt; &gt; &gt;
<br>&gt; &gt; &gt; What I find missing is static checking if contracts are
<br>&gt; &gt; &gt; satisfied. You cannot standardize automatic bug detectio=
n,
<br>&gt; &gt; &gt; but you can make sure that programmers have enough means=
 to
<br>&gt; &gt; &gt; convey their intent to static analysers and such. Withou=
t such
<br>&gt; &gt; &gt; support contract programming features appear incomplete.=
 At
<br>&gt; &gt; &gt; least in the sense that certain static transformations a=
re
<br>&gt; &gt; &gt; performed, but it is not checked if they are safe.
<br>&gt; &gt;
<br>&gt; &gt; I don't see why the ability to do static checking of contract=
s
<br>&gt; &gt; does not fall out of pretty much any contract proposal. &nbsp=
;Consider
<br>&gt; &gt;
<br>&gt; &gt; type* producer();
<br>&gt; &gt; void consumer(type* arg) preconditon { arg !=3D NULL };
<br>&gt; &gt; ....; consumer(producer()); ....
<br>&gt; &gt;
<br>&gt; &gt; The compiler that the postcondition of the call to producer
<br>&gt; &gt; is insufficient to satisfy the precondition of the call to
<br>&gt; &gt; the consumer. &nbsp;A tool can can warn in this case.
<br>&gt; &gt;
<br>&gt; &gt; On the other hand, in
<br>&gt; &gt;
<br>&gt; &gt; type* producer() postcondition { result !=3D NULL; };
<br>&gt; &gt; void consumer(type* arg) preconditon { arg !=3D NULL; };
<br>&gt; &gt; ....; consumer(producer()); ....
<br>&gt; &gt;
<br>&gt; &gt; the postcondition easily satisfies the precondition. &nbsp;Th=
e
<br>&gt; &gt; compiler can avoid generating the precondition check based on
<br>&gt; &gt; that satisfiability.
<br>&gt;
<br>&gt; True, if one function's postcondition is _exactly_ same as other
<br>&gt; function's precondition, then static analyser can exploit this in
<br>&gt; any contract programming framework. The situation is different whe=
n
<br>&gt; preconditions and postconditions cannot be matched exactly. For
<br>&gt; instance, one function ensures property *is_positive(e)*
<br>&gt; and another requires property * is_nonnegative(e)*. The former
<br>&gt; implies the latter, but the analyser would not know it.
<br>
<br>If is_positive(e) and is_nonnegative(e) are inline functions
<br>implemented as e&gt;0 and e&gt;=3D0, then the compiler certainly can ma=
ke the
<br>proper inferences. &nbsp;In any case, the compiler can only manipulate
<br>predicates that are within its algebraic domain, and so it would
<br>be best if preconditions were written to a reasonable domain.
<br>
<br>&gt; Similarly, there could be more than one way of stating the
<br>&gt; same state. In case of pointer, it is *bool(p)* and *p !=3D
<br>&gt; nullptr*. Because pointers are built into the language
<br>&gt; compilers/analysers can understand the "redundancy" in the
<br>&gt; interface, but in similar case of *std::optional*, automated
<br>&gt; tools will not know that* bool(o) *is equivalent to* o !=3D nullop=
t*.
<br>
<br>But if the postcondition on bool(o) is result =3D=3D (o!=3Dnullopt),
<br>then that interpretation is within reach. &nbsp;It will take work to
<br>specify preconditions and postconditions in a manner that is both
<br>useful to compilers and to programmers.
<br>
<br>&gt; My personal opinion is that this element would be really missing
<br>&gt; from a "toolset" for enhancing static analysis. And on the other
<br>&gt; hand a construct for expressing such relationships has already
<br>&gt; been devised. Whether this ability is essential or not for the
<br>&gt; first "pass" of contract programming enhancements is I guess
<br>&gt; very subjective.
<br>
<br>I am not sure that we are all that far from what you suggest, at
<br>least for a reasonable subset of the preconditions. &nbsp;Can you write
<br>a paper describing what you want in detail?
<br></blockquote><div><br>I describe some examples of what I mean in the fo=
llowing draft paper:<br><a href=3D"http://htmlpreview.github.io/?https://gi=
thub.com/akrzemi1/contract/blob/master/contract.html" target=3D"_blank">htt=
p://htmlpreview.github.io/?<wbr>https://github.com/akrzemi1/<wbr>contract/b=
lob/master/contract.<wbr>html</a> <br><br>Regards,<br>&amp;rzej<br></div></=
div>

<p></p>

-- <br />
<br />
--- <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 />
Visit this group at <a href=3D"http://groups.google.com/a/isocpp.org/group/=
std-proposals/">http://groups.google.com/a/isocpp.org/group/std-proposals/<=
/a>.<br />

------=_Part_10_11299482.1404897813754--

.