Question

For the function definition int SomeFunc( /* in */ int alpha, /* in */ int beta ) { int gamma; alpha = alpha + beta; gamma = 2 * alpha; return gamma; } what is the function postcondition?

Answer 1

function value == 2*(alpha@entry + beta@entry)

Step-by-step explanation:

int SomeFunc( /*in */ int alpha, /* in */ int beta )

{

int gamma;

alpha = alpha + beta;

gamma = 2 * alpha;

return gamma;

}

The post-condition is useful for testing purposes. It represents what value the function SomFunc is expected to return at the time of program execution in a simplified manner.

For the given problem the post-condition is

function value == 2*(alpha@entry + beta@entry)

Where @entry represents the value of alpha and beta at the moment when the function was called.

Note: /*in */ it represents comment in c++ language and is ignored by the compiler

Answer 2

A function post-condition refers to what will happen and return after calling the function.

Given the function definition as follows:

1. int SomeFunc( /* in */ int alpha, /* in */ int beta )
2. {
3. int gamma;
4. alpha = alpha + beta;
5. gamma = 2 * alpha;
6. return gamma;
7. }

If we call the function by passing two values, 3 and 4, as input parameters, the 3 will be captured by alpha and 4 by beta. The two input values will by calculated based on the formula defined inside the function as follows:

alpha = 3 + 4 = 7

gamma = 2 * 7 = 14

At last the function will return 14.