8

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

10
  • 9
    It is actually "the function f returns maximum of its arguments when they are not equal and second argument when they are equal". Jan 8, 2018 at 13:50
  • 1
    and when a=b, max(a,b)=a=b
    – Adam
    Jan 8, 2018 at 14:13
  • 3
    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.
    – Davislor
    Jan 8, 2018 at 15:46
  • 1
    @Davislor 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 ∀ yS . xy, 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)
    – Daniel H
    Jan 8, 2018 at 16:55
  • 1
    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?
    – Davislor
    Jan 8, 2018 at 17:13

3 Answers 3

4

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.

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.

1
+50

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.

Your Answer

Reminder: Answers generated by Artificial Intelligence tools are not allowed on Stack Overflow. Learn more

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.