Take the following C++14 code snippet:
unsigned int f(unsigned int a, unsigned int b){
if(a>b)return a;
return b;
}
Statement: the function f
returns the maximum of its arguments.
Now, the statement is "obviously" true, yet I failed to prove it rigorously with respect to the ISO/IEC 14882:2014(E) specification.
First: I cannot state the property in a formal way.
A formalized version could be: For every statement s, when the abstract machine (which is defined in the spec.) is in state P and s looks like "f(expr_a,expr_b)" and 'f' in s is resolved to the function in question, s(P).return=max(expr_a(P).return, expr_b(P).return).
Here for a state P and expression s, s(P) is the state of the machine after evaluation of s.
Question: What would be a correctly formalized version of the statement? How to prove the statement using the properties imposed by the above mentioned specification? For each deductive step please reference the applicable snippet from the standard allowing said step (the number of the segment is enough).
Edit: Maybe formalized in Coq
Please appologize for my approximate ageing mathematic knowledge.
Maximum for a closed subset of natural number (BN) can be defined as follow:
Max:(BN,BN) -> BN
(x ∊ BN)(a ∊ BN)(b ∊ BN)(x = Max(a,b)) => ( x=a & a>b | x=b )
where the symbol have the common mathemical signification.
While your function could be rewritten as follow, where UN is the ensemble of unsigned int
:
f:(UN,UN) -> UN
(x ∊ UN)(a ∊ UN)(b ∊ UN)(x = f(a,b)) => ( x=a && a>b || x=b )
Where symbol = is operator==(unsigned int,unsigned int)
, etc...
So the question reduces to know if the standard specifies that the mathematical structure(s) formed by the unsigned integer
with C++ arithmetic operators and comparison operator is isomorphic to the matematical structures (classes,categories) formed by a closed subset of N with the common arithemtic operation and relations. I think the answer is yes, this is expressed in plain english:
C++14 standard,[expr.rel]/5 (Relational Operators)
If both operands (after conversions) are of arithmetic or enumeration type, each of the operators shall yield
true
if the specified relationship is true andfalse
if it is false.
C++14 standard, [basic.fundamental]/4 (Fundamental Types)
Unsigned integers shall obey the laws of arithmetic modulo 2n where n is the number of bits in the value representation of that particular size of integer.
Then you could also proove that ({true
,false
},&&
,||
) is also isomorphic to boolean arithmetic by analysing the text in [expr.log.and]
and [expr.log.or]
I do not think that you should go further than showing that there is this isomorphism because further would mean demonstrating axioms.
It appears to me that the easiest solution is to prove this backwards. If the first argument to f
is the maximum argument, prove that the first argument is returned (fairly easy - the maximum argument a
is by definition bigger than b
). If the second argument is the maximum argument, prove that the second argument is returned. If the two are equal, show that there is no unique maximum element, so the second argument is still a maximum argument.
Finally, prove that these three options are exhaustive. If a unique maximum argument is passed, it must be passed either as the first or the second argument, since f
is binary.
I am unsure about what you want. Looking at a previous version, N3337, we can easily see that almost everything is specified:
However, you attempt to start with f(expr_a, expr_b); and evaluating the arguments to f potentially requires a lot more; especially since they are not sequenced - and could be any function-call.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With