Specifying Functions¶

describing what a function does is called specifying the function

when we write the body of a function with a specification, we say that we are implementing the specification, or meeting the specification

for example, suppose we want to write a function called max_index that returns the position of the max value in a vector<double> v

A Bad Specification¶

we could specify it informally with the English phrase “max_index(v) returns the index of the biggest number in v”

we could write it in code like this:

// Returns the index of the biggest number in v.
int max_index(const vector<double>& v) {
    // ...
}

notice the specification doesn’t say anything about how the function works, i.e. it’s body is empty

a good specification only says what a function does, and leaves how it does it up to the programmer

how good is this specification?

it turns out to have a couple of big problems

what’s the max of an empty vector<double>?

what if 2, or more, numbers are tied for the biggest?

e.g. in {1, 2, -3, 2} should the index 1 or 3 be returned?

so we need to change the specification so it says what to do in these cases

A Better Specification¶

the simplest fix to the specification is to add some sentences saying exactly what to do in the two problem cases, e.g.:

// Returns the index of the biggest of v. If v is empty, an exception is
// thrown. If the max occurs two, or more, times, then the position of the
// left-most max is returned.
int max_index(const vector<double>& v) {
    // ...
}

this is better — the person implementing this function now knows what to do in every case

however, informal English like this is hard to read and write

more structured specifications are thus useful

Pre-conditions and Post-conditions¶

here is the specification for max_index re-written using a pre- condition and a post-condition:

// Pre-condition:
//    v.size() > 0
//
// Post-condition:
//    Returns i such that v[i] is the largest element in v,
//    and any elements before v[i] are less than v[i].
int max_index(const vector<double>& v) {
    // ...
}

the pre-condition asserts what the function assumes is true before it is called

the post-condition asserts what the function promises will be true after the function is called (assuming the pre-condition was true when it was called)

together, the pre-condition and post-condition act like a contract between the function and the rest of the program

from now on, we’ll use pre-conditions and post-conditions to specify trick or important functions

Pre-condition and Post-condition Example: min¶

write the specification for min(x, y), i.e. the function that returns the smaller of x and y:

// Pre-condition:
//    none
//
// Post-condition:
//    Returns the smaller of x and y.
int min(int x, int y) {
    // ...
}

there’s no pre-condition here, which means that you can call min with any x and y and it should work

Pre-condition and Post-condition Example: absolute value¶

write the specification for abs(x), i.e. the function that returns the smaller of the int x:

// Pre-condition:
//    x != min int
//
// Post-condition:
//    If x < 0, returns -x. Otherwise, returns x.
int abs(int x) {
    // ...
}

the pre-condition indicates that abs will not work correctly for the minimum possible int

recall that there is one more negative number than positive number in the usual encoding of numbers as ints, so there is no way for abs to return the correct absolute of the min int

Pre-condition and Post-condition Example: vector equality¶

write the specification for equals(v, w), i.e. the function that tests if two vectors<string>s are equal:

// Pre-condition:
//    none
//
// Post-condition:
//    Returns true just when v.size() == w.size(), and
//    v[0] == w[0], v[1] == w[1], ..., v[v.size()-1] == w[v.size()-1].
bool equals(const vector<string>& v, const vector<string>& w) {
    // ...
}

again there is no pre-condition, meaning that equals should work with any two vector<string>s

we could have said that v and w must both contain strings, but in C++ the function header enforces that, so there’s no need to repeat in the pre- condition

Pre-condition and Post-condition Example: printing a box¶

write the specification for box(w, h, c), i.e. a function that prints, on cout, h lines each consisting of w c characters (and ending with \n)

e.g. box(3, 5, '+') prints this on cout:

+++
+++
+++
+++
+++


// Pre-condition:
//    width > 0, height > 0
//
// Post-condition:
//    Prints, on cout, height rows of exactly width c characters each.
//    Each row should end with a '\n'.
//
// Note:
//    For some characters c, you might not see a box, e.g. if c == '\n',
//    then most likely many blank lines will be printed.
//
//    There is no max value for width or height, but if you print a box that's
//    wider than your screen it might not look like a box. Similarly, if your
//    box is higher than the number of lines on your screen, the screen might
//    scroll.
void box(int width, int height, char c) {
    // ...
}

notice that we added a “note” section the specification, mentioning some possible problems with the function

it’s possible that the notes part could be made part of the pre-condition, e.g. you could specify in the pre-condition that c must be “printable on cout”, but what “printable” means is unclear, and may depend upon the situation

Pre-condition and Post-condition Example: what does this function do?¶

suppose you have a function returns_zero() that, when you call it, always returns 2, e.g.:

returns_zero() returns 2
returns_zero() returns 2
// ...

is returns_zero() working correctly?

we don’t know for sure — it depends upon its specification, i.e. it depends upon what returns_zero() is supposed to do

one possible specification is this:

// Pre-condition:
//    none
// Post-condition:
//    always returns 2
int returns_zero()

if this is the specification for returns_zero, then it is indeed working correctly!

the name, of course, is terribly mis-leading — it should be changed to returns_two

however, suppose its specification was this:

// Pre-condition:
//    none
// Post-condition:
//    always returns 0
int returns_zero()

now the specification says that 0 should be returned, so if returns_zero always returns 2, it is wrong

in practice, this kind of problem is quite common (and never so obvious!)

just because a function has no obvious bugs doesn’t mean it does what the specification requires it to do!

also, in real life, it’s quite possible the specification itself is wrong — maybe the person writing it accidentally typed a 2 instead of a 0

Specifying a Sort Function¶

sorting data into ascending order is one of the most common and important tasks done by computers

sorting {4, 0, 3, 2, 2, 1} gives {0, 1, 2, 2, 3, 4}

sorting {"zebra", "cow", "mouse", "fly"} gives {"cow", "fly", "mouse", "zebra"}

Specifying a Sort Function: the wrong way¶

here’s a wrong specification for sorting:

// Pre-condition:
//    none
//
// Post-condition:
//    v[0] <= v[1] <= v[2] <= ... <= v[v.size()-1]  (wrong!)
void sort(vector<int>& v) {
    // ...
}

the post-condition should indeed be true after calling sort

but it’s too permissive — the post-condition allows sort to do things we didn’t intend

suppose v = {2, 1, 3}, and after calling sort(v), v has been changed to {0, 0, 0, 7}

it’s obviously not sorting correctly, but the post-condition is satisfied!

the problem is that the specification doesn’t say that the elements of v must be permuted, i.e. re-arranged without otherwise adding or removing any elements

Specifying a Sort Function: the right way¶

here’s a correct specification for sorting:

// Pre-condition:
//    none
//
// Post-condition:
//    Permutes the elements of v such that         (correct!)
//    v[0] <= v[1] <= v[2] <= ... <= v[v.size()-1]
void sort(vector<int>& v) {
    // ...
}

Invariants¶

pre-conditions and post-conditions are examples of the more general idea of code invariants

an invariant is a fact that is true at some point in a program

invariants can be helpful when developing loops, i.e. finding a useful invariant for a loop is a one way to help ensure the loop works correctly

Invariants: max_index¶

here’s the specification of the max_index function from before:

// Pre-condition:
//    v.size() > 0
//
// Post-condition:
//    Returns i such that v[i] is the largest element in v,
//    and any elements before v[i] are less than v[i].
int max_index(const vector<double>& v) {
    // ...
}

let’s write the body:

int mi = 0;  // mi is the index of the max value seen so far
for(int i = 1; i < v.size(); ++i) {   // note that i starts at 1
    //
    // what's true at this point?
    //
    if (v[i] > v[mi]) {
       mi = i;
    }
}
return mi;

what invariants could we put at the top of the loop body?

we could add trivial invariants like these

2 == 2
i >= 1 and i < v.size()

while these are true, they are not useful

instead, this is a little more useful: v[mi] is the max of v[0], v[1], … v[i-1]

it says that v[mi] is the max of all the elements that come before v[i]

the if-statement that comes after this invariant guarantees that the invariant is true next time through the loop

int mi = 0;  // mi is the index of the max value seen so far
for(int i = 1; i < v.size(); ++i) {   // note that i starts at 1
    //
    // invariant: v[mi] is the max of v[0], v[1], ... v[i-1]
    //
    if (v[i] > v[mi]) {
       mi = i;
    }
    //
    // invariant: v[mi] is the max of v[0], v[1], ... v[i]  (i instead of i-1)
    //
}
return mi;

Specifying Performance¶

the speed and memory-usage of functions is a major topic in programming and computer science

everyone wants faster programs that use less memory

specifying the performance or memory usage of a function turns out to be rather tricky, and so we will come back to this topic later

Table Of Contents

Previous topic

Next topic