Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Rigorous proof of the following C++ code's property?

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

like image 674
Adam Avatar asked Jan 08 '18 13:01

Adam


3 Answers

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

like image 70
Oliv Avatar answered Nov 15 '22 03:11

Oliv


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.

like image 41
MSalters Avatar answered Nov 15 '22 02:11

MSalters


I am unsure about what you want. Looking at a previous version, N3337, we can easily see that almost everything is specified:

  • a and b starts with the calling values (Function 5.2.2 - 4)
  • Calling a function executes the compound statement of the function body (Obvious, but where?)
  • The statements are normally executed in order (Statements 6)
  • If-statements execute the first sub-statement if condition is true (The If Statement 6.4.1)
  • Relations actually work as expected (Relation operators 5.9 - 5)
  • The return-statement returns the value to the caller of the function (The return statement 6.6.3)

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.

like image 1
Hans Olsson Avatar answered Nov 15 '22 02:11

Hans Olsson