一、实验题目： 实验4 程序的形式化推导

二、实验内容：

（1）　　根据给定的问题，建立前置谓词和后置谓词。

（2）　　根据条件语句的推导策略，建立程序中的条件语句。

（3）　　构造循环不变式，确立界函数。

（4）　　根据循环语句的推导策略，建立程序中的循环语句。

（5）　　面向目标，退到出所要的程序。

三、实验目的

根据条件语句的推导策略和循环语句的推导策略，基于最弱前置条件的概念，用比较形式化的方法，从设计要求达到的目标一步步推导出程序。

四、实验要求：

运用C++，编写一个程序实现N的阶乘。

运用循环不变式设计。

-First, the experimental subjects: Formal test procedures derived 4

Second, experimental elements:

(1) According to a given problem, the establishment of pre-and post-predicate predicate.

(2) Derivation of conditional statements in accordance with the strategy, the establishment of procedures for the conditional statements.

(3) loop invariant structure, the establishment of community function.

(4) According to the derived loop strategy, the establishment of procedures for the circulation statement.

(5) goal-oriented, back to the process.

Third, the experiment was

Derivation of conditional statements in accordance with the strategy and the derived loop strategy, based on the concept of the weakest pre-conditions, a more formal way, from design requirements to achieve a step-by-step procedures derived.

Fourth, the experimental requirements:

　　The use of C++, the preparation of a program to achieve the factorial N.

　　Design of the use of loop invariants.