c# - 函数/方法的后置条件

Question

你们中有人曾经用前置条件和后置条件记录过函数或方法吗？ (我问是因为我的老师说这是官方/正确的方法):

图例:(因为我无法输入特殊字符)3 - 读作“存在” '&exist'
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]    

这是等待后置条件的先决条件;)

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) ]  

你们中有人在现实世界中遇到过这种记录函数/方法的方法吗？

Answer 1

是的。我遇到过它，尽管这不是行业中的常规做法。

在某些情况下，正式指定 preconditions 绝对算作最佳实践 , postconditions和 invariants .例如:

• 使用 formal methods 时;例如正式证明程序是正确的，或者
• 使用像 Eiffel 这样支持 design by contract 的编程语言时.

如果您想了解 Eiffel 语言如何支持契约(Contract)设计的示例，请查看 here .

---

顺便说一句，倒转 E 表示“存在”，倒转 A 表示“所有”，这是标准的数学符号，如果你学过一年级的大学数学类(class)，你就会遇到它们。人们使用的正式方法是种类或符号，这(可以说)有点不幸。它不必要地推迟/吓跑了绝大多数(通常)对数学感到不舒服的程序员。