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

Question

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

Subordinary

It is actually "the function f returns maximum of its arguments when they are not equal and second argument when they are equal". – Jaquith

and when a=b, max(a,b)=a=b – Subordinary

The C language standard formally allows an implementation to support distinct +0 and -0 values of int such that +0 and -0. may compare equal. All modern computers just use two’s-complement signed numbers, but some early CPUs supported one’s-complement or sign-and-magnitude arithmetic where that makes sense. IEEE floating-point explicitly has +0.0 and -0.0. – Minimalist

A formal statement might be: x is the maximum of a set S iff x ∈ S ∧ ∀ y ∈ S . x ≥ y. Without the first condition, x is the supremum of S. In this case, S has two elements. – Minimalist

@Minimalist Without the first condition, x isn’t even necessarily the supremum. For the set S = {∑ⁿᵢ₌₀ 2ⁱ| n ∈ ℕ} = {1,1.5,1.75,1.875,...} and x = 17, we have ∀ y ∈ S . x ≥ y, but y is definitely not the supremum. (This works for finite sets too, but is clearer with infinite sets because only then do people usually talk about suprema) – Cavern

@DanielH You’re right; the supremum must of course be the least upper bound, and the second condition is just the definition of upper bound. Doesn’t matter here, but then I shouldn’t have brought it up. – Minimalist

Anyway, from your feedback to my deleted answer, it sounds like what you’re asking for is not a rigorous definition of maximum and proof in conventional notation that the property holds after executing either branch, but advice on how to word the proof to a particular standard? Are there good examples of the kind of proof you want, that you can imitate? – Minimalist

You might want to check out Frama-C (which has only experimental C++ support and by default doesn’t conform precisely to the C standard with e.g. signed integer overflow, but is a place to start if you want practical proofs of correctness). The seL4 kernel also has proofs of C semantics in Isabelle/HOL, but as far as I can tell they don’t have a generally-available tool for converting C to something Isabelle/HOL can understand and you’d need to try to use their C parser with relatively little documentation. – Cavern

I do not know of a mechanized C++ library in a proof assistant like Coq, though there has been work (by Tahina Ramanandro, Gabriel Dos Reis, Xavier Leroy et al.) on defining subsets of such semantics. This is maybe provable for C semantics, using: vst.cs.princeton.edu But you might end up reasoning about an encoding of the function you care about in their logic, rather than directly the syntactic version of the code you provided here. I am not sure whether they have parsing facility to parse concrete C code. – Kloof

The one other piece of advice I have for approach is that the transformation to static single assignment form defines ϕ functions to replace conditional assignments such as this, and you might take advantage of this notation (or the equivalence to (a>b) ? a : b) to write your proof elegantly. – Minimalist

Answer 1

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.

Profound

Answer 2

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.

Leander

Answer 3

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.

Overwrite