Постусловие для функции / метода

Кто-нибудь из вас когда-либо документировал функцию или метод с предварительными и пост-условиями ? (Я спрашиваю, потому что мой учитель говорит, что это официальный / правильный способ сделать это):

Легенда: (потому что я не мог вводить специальные символы)

Кто-нибудь из вас когда-либо документировал функцию или метод с предварительными и пост-условиями? (Я спрашиваю, потому что мой учитель говорит, что это официальный / правильный способ сделать это):

Легенда: (потому что я не мог вводить специальные символы)

Кто-нибудь из вас когда-либо документировал функцию или метод с предварительными и пост-условиями? (Я спрашиваю, потому что мой учитель говорит, что это официальный / правильный способ сделать это):

Легенда: (поскольку я не мог вводить специальные символы) 3 - прочтите это как «существует» «и существует»
E - член (как в наборе)
A - для всех
-> - подразумевает

Предположим, что s - непустая строка. Пусть B (s) будет набором целых чисел, которые задают индексы позиций в строке s.
Здесь начинается документация этой функции:

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

это предварительное условие 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) ]  

Кто-нибудь из вас когда-либо сталкивался с таким способом документирования функций / методов в реальном мире?