有许多方法可以表示程序的结构（如 UML 类图等）。我很感兴趣是否有一个以严格的数学方式描述程序的约定。我对为此目的使用数学符号特别感兴趣。
示例：类表示为集合（字段、属性）和函数（对集合的元素进行操作）。父类的字段是子类的子集。函数是用伪代码描述的，伪代码必须看起来像这样那样......
There are many methods for representing structure of a program (like UML class diagrams etc.). I am interested if there is a convention which describes programs in a strict, mathematical way. I am especially interested in the use of mathematical notation for this purpose.
An example: Classes are represented as sets (fields, properties) and functions (operating on the elements of sets). A parent class' fields are a subset of child class'. Functions are described in pseudocode which has to look like this and that...
发布评论
评论（10）
我知道Z Notation已经在软件的形式化验证中得到了一定程度的使用，比如Tokeneer项目。
I know that Z Notation has been used to some extent in the formal verification of software, such as the Tokeneer project.
http://www.amazon.com/Concrete-Mathematics-Foundation-Computer-Science/ dp/0201558025
http://www.amazon.com/Concrete-Mathematics-Foundation-Computer-Science/dp/0201558025
是的，有，弗洛伊德霍尔逻辑。
Yes, there is, Floyd-Hoare Logic.
有很多方法，但我认为大多数方法都不方便表达结构，因为结构通常无法用默认的数学概念来表达。主要的例外当然是函数式编程语言。想想折叠（变形）、群、代数等。
对于命令式编程，我知道 Z 的存在，它使用（纯和扩展）lambda 演算集合论和（一阶）谓词逻辑。但是，我认为这不是很方便。使用数学来表达结构的唯一好处是你可以证明有关它的东西。但如果您想这样做，请查看 JML、Spec# 或 Eiffel。
There are a lot of way, but i think most of them are inconvenient for expressing the structure since the structure is often not expressable in default mathematical concepts. The main exception is of course functional programing languages. Think about folds (catamorphisme), groups, algebra's etc.
For imperative programming I know of the existence of Z, which uses (pure and extended) lambda calculus set theory and (first order) predicate logic. However, i dont think it's very convenient. The only upside of using mathematics to express structure is the fact that you can prove stuff about it. But if you want to do that, take a look at JML, Spec# or Eiffel.
取决于您想要实现的目标，但是使用特定语言走这条路可能会给您带来麻烦。
例如，请参阅有关 C++ 常见问题解答的圆-椭圆讨论精简版。
Depends on what you're trying to accomplish, but going down this road with specific languages can get you into trouble.
For example, see the circle-ellipse discussion on C++ FAQ Lite.
我相信 Alexander Stepanov 和 Paul McJones 的编程元素非常接近你正在寻找。
I believe that Elements of Programming by Alexander Stepanov and Paul McJones, is pretty close to what you are looking for.
Z，已经提到过，几乎就是你所描述的。它有一些用于面向对象建模的变体，但我认为如果您希望对类进行建模，您可以使用“标准 Z ”模式走得很远。
还有 Alloy，它是较新的，受 Z 启发。它的表示法可能更接近面向对象。它也是可分析的，即你可以检查你创建的模型是否满足某些条件，但它不能证明属性成立，只是试图在有限的范围内反驳。
可靠软件设计一文很好地介绍了 Alloy 及其同类产品，以及可用的类似工具的表格。
Z, which has already been mentioned, is pretty much what you describe. There are some variants of it for object-oriented modelling, but I think you can get quite far with "standard Z's" schemas if you wish to model classes.
There's also Alloy, which is newer and inspired by Z. Its notation is perhaps a bit closer to object-orientation. It is also analysable, i.e. you can check the models you create whether they fulfill certain conditions, but it cannot prove that properties hold, just attempt to refute within a finite scope.
The article Dependable Software by Design is a nice introduction to Alloy and its ilk, along with a table of available similar tools.
您正在寻找函数式编程。有多种函数式编程语言，它们都基于称为Lambda 演算的基本数学理论。用函数式编程语言（例如 LISP）编写的程序是其自身的数学表示。 ;-)
You are looking for functional programming. There are several functional programming languages, and they are all based on a fundamental mathematical theory called the Lambda calculus. Programs written in a functional programming language such as LISP are a mathematical representation of themselves. ;-)
有一种数学语言实际上描述了程序或更确切地说是它的操作。您采用初始状态，然后转换该状态，直到达到所需的目标状态。转换产生必须执行的程序代码。
请参阅有关霍尔逻辑的维基百科文章。
基本思想是，对于每个函数（无论将其放入类中还是旧式函数中），都有一个前置条件和一个后置条件。例如，前提条件可以是您有一个包含
>= 0元素的数组。后置条件是对于每个 i <= j，每个 element[i] 必须 <= element[j]。通常的描述是“函数对数组进行排序”。但数学术语允许您将输入（必须与前置条件匹配）转换为输出（必须与后置条件匹配）。
它使用起来有点笨拙，特别是对于更复杂的程序，但一些示例非常令人印象深刻。通常，您会得到非常紧凑的代码，结果看起来相当复杂，但第一次尝试就可以工作。
There is a mathematical language which actually describes a program or rather it's operations. You take the initial state and then transform this state until you reach the desired target state. The transformations yield the program code which must be executed.
See the Wikipedia article about Hoare logic.
The basic idea is that for every function (no matter if you put that into a class or into an old style function), you have a pre- and a post-condition. For example, the precondition can be that you have an array which has
>= 0elements. the post-condition is that every element[i] must by <= element[j] for every i <= j.The usual description would be "the function sorts the array". But the mathematical terms allow you to transform the input (which must match the precondition) into the output (which must match the postcondition).
It's a bit unwieldy to use, especially for more complex programs but some of the examples are pretty impressive. Often, you get really compact code as the result which looks quite complex but works at first try.
我想推荐编程代数。这是一种使用关系代数和伽罗瓦连接。
如果您对这个主题有进一步的兴趣，您可以找到一篇精彩的论文，此处，作者：Shin-Cheng Mu 和 José Nuno Oliveira (幻灯片）。
使用关系代数和一阶逻辑，还与 Alloy、函数式编程和契约设计有很好的协同作用（很容易应用于面向对象编程）。
I'd like to suggest Algebra of Programming. It's a calculational approach to programs, using Relational Algebra, and Galois Connections.
If you have further interest on this topic, you can find an amazing paper, here, by Shin-Cheng Mu, and José Nuno Oliveira (slides).
Using Relational Algebra and First-Order Logic, also has a nice synergy with Alloy, Functional Programming, and Design by Contract (easily applied to Object-Oriented Programming).