Post-condition for a function/method

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?

---

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.

---

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

---

Spec# documents post conditions as follows:

static void Main(string![] args)
    requires args.Length > 0
{
    foreach(string arg in args)
    {
        Console.WriteLine(arg);
    }

---

I have written pre and post conditions, and class invariants, in a formal way. The problem with it arises when there's no critical mass understanding formal notations.

I must admit that it takes me longer to understand A i in B(s): i < FirstOcc --> s[i] != c than simply: s has no occurence of c before firstOccurence(s,c).

The formalism is only useful when

1. 'intuitive' understanding of the function becomes too hard. Then, you can only fall back onto formal methods to prove correct implementation or usage.
2. automatic verification is required

Take a look at e.g. the sgi/stl documentation. They use semi-formal notations, too, and all too often I see people struggling to grasp the meaning of the thus documented functions.

---

Cofoja (Contracts for Java) provides Eiffel like contracts by using annotations.

  @Requires({
    "h >= 0",
    "h <= 23"
  })
  @Ensures("getHour() == h")
  void setHour(int h);