Post-condition for a function/method

Question

Did anyone of you ever documented a function or method with pre and post conditions? (I'm asking because my teacher says that's the official/correct way to do it):

Legend: (for I couldn't type special chars) 3 - read it as "there exists" '&exist'
E - is a member of (as in set)
A - for all
--> - implies

Suppose that s is a non-empty string. Let B(s) be the set of integers that give the indices of positions in the string s.
Here starts documentation of this function:

int FirstOccurence(String s, Char c)   
precondition: 
  (s.lenght() > 0) && 3 int i in B(s) [s.charAt(i) == c]    

that's the precondition wait for postcondition ;)

postcondition: 
  (FirstOccurence(s,c) E B(s)) && (s.charAt(FirstOccurence(s,c)) == c) && 
     A int i B(s)[(i < FirstOccurence(s,c)) --> !(s.charAt(i) == c) ]  

Did any one of you ever came across such a way of documenting functions/methods in a real world?

Answer 1

Yup. I've come across it, though it is not normal practice in industry.

In certain context, it would definitely count as best practice to formally specify the preconditions, postconditions and invariants. For example:

• when using formal methods; e.g. for formally proving that programs are correct, or
• when using a programming language like Eiffel that supports design by contract.

If you want an example of how the Eiffel language supports design by contract, look here.

---

BTW, backwards E for 'there exists' and upside down A for 'for all' are standard mathematical notation, and you would have encountered them if you had done 1st year University Maths courses. It is (arguably) somewhat unfortunate that formal methods folks use is kind or notation. It it unnecessarily puts off / scares off the vast majority of programmers who are (in general) uncomfortable with maths.

Answer 2

I have also used it at the university, and when documenting some functions where I find it useful.

In the "real" world it's not so common (well in general, people doesn't document so much).

I think any documentation is good, and in cases where it's not very clear the status of the input/output parameters before and after the function, a precondition and a postcondition is the way to go.

By the way, in HTML you can use ∃ --> ∃ ∀ --> ∀ and some other character entities: http://en.wikipedia.org/wiki/List_of_XML_and_HTML_character_entity_references