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

Answer:

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.

Answer 2

Answer:

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

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