Research On Some Problems About Proving The Correctness Of Programming

The development of computer software is affected by many factors and is delayed comparing with hardware. The safety, reliability and stability of software have been important problems and attracted people's much attention for a long time.With the fast development of the huge software as well as the high safety demand from high technique such as spaceflight and aviation design, the quality of software, especially the correctness of software,has become more and more important. Therefore, the proof of the correctness of software and the test of software have been attractive research fields. The aim of proof of the correctness of software is to ensure that there is no errors in program and to meet the demands of the users. On the other hand, the aim of test of software is to find possible errors in program. Both are closely related to the whole life cycle of software. However, they are essentially different with each other. There have been developed various kinds of models such as the computable function model, predicate word calculus, Turing machine, algebra model etc.in the related fields. Each model has its one advantage and limitation. It is practically impossible to use only one model to solve the reliability problems due to its complexity. The core of a program is a finite state machine(FSM). In this thesis we discuss several deferent kinds of FSM model including the tradition FSM and the currrently popular state machine in UML(Unified Modeling Language). We propose a matrix model of FSM. We then use pure mathematical method as a tool to analyze related problems in the fields of computer and derive related algebraic properties. By the use of complete algebra theory, we discuss algebraic problems concerned with computer theory. These problems include the reliability, the completeness and the solvability etc. Meanwhile, with the help of the Object-oriented design theory, we discuss the extensibility mechanism in UML language. In other words, we study the reliability from the source of design.In this thesis, we study the correctness of program from the following aspects:1 .The definition of the correctness of program. So far, there is not a strict definition about the correctness of program. In this thesis, we give a strict definition and point out some misunderstanding formed for a long time.2.The correctness of model. We discuss the use case and state machine of UML in this thesis. Use case is useful not only for testing, but also for modeling. The problem of use case is generally very large. As a result.it brings difficulty in the construction of the model and the test of program. We discuss the amount of use case about stack, and obtain a recurrence formula. The state machine in UML is different from the traditional FSM. In this thesis, we establish a model that combines the statechart diagram with traditional FSM. It provides a convenient tool to code efficient and reliable programs.3.Types system and correctness of types system. Types system is part of program language. It follow the tracks type of the variables including types of expressions. Checking of type could ensure the correctness of program. We analyze finite bases in classic algebra and obtain a conclusion that congruence-permutable algebra varieties has finite equation bases. By means of matrix model for Turing machine, we derive an algebra that posseses solvable word problems but not recursively solvable word problems. We study the soundness and complement of the types system, In addition,we establish a theorem for the types system to be soundness4.Correctness of programs language and the algorithms. We study correctness of program language and give a way to solve the correctness of the cycle structure program. After giving the good side effect idea we get the results that side effect of applicative language is not good and that side effect of imperative language after adding assign sentence is good.