Martin-Löf's type theory is a theory in which one can write both specifications and programs. By interpreting propositions as types, predicate logic is available when formulating a specification. The rules of...
详细信息
Martin-Löf's type theory is a theory in which one can write both specifications and programs. By interpreting propositions as types, predicate logic is available when formulating a specification. The rules of type theory are formulated as tactics which makes a “top down” construction of programs possible. These ideas are illustrated by a formal derivation of a program for a partitioning problem.
The state of the art in the area of program verification is now reaching a stage in which many of the existing results on analysis of programs are starting to be transferred to practice through research on software en...
详细信息
The state of the art in the area of program verification is now reaching a stage in which many of the existing results on analysis of programs are starting to be transferred to practice through research on software engineering. Efforts are now turning to the goal of providing a methodology for the systematic synthesis of programs, and many people are working on the problem of deriving a program from a given program *** program derivation process can be summarized as: 1. the choice of a suitable data type, 2. the statement of some properties of the type, 3. the derivation of the program schema, 4. the choice of a data representation and definition of the data type in terms of this representation, 5. proof of the correctness of the representation, and 6. derivation of the cluster. The concept of a cluster is instrumental for providing a programming mechanism for the encoding of the data representation.
Relative correctness is the property of a program to be more-correct than another program with respect to a given specification. Among the many properties of relative correctness, that which we found most intriguing i...
详细信息
Relative correctness is the property of a program to be more-correct than another program with respect to a given specification. Among the many properties of relative correctness, that which we found most intriguing is the property that program P' refines program P if and only if P' is more-correct than P with respect to any specification. This inspires us to reconsider program derivation by successive refinements: each step of this process mandates that we transform a program P into a program P' that refines P, i.e. P' is more-correct than P with respect to any specification. This raises the question: why should we want to make P' more-correct than P with respect to any specification, when we only have to satisfy specification R? In this paper, we discuss a process of program derivation that replaces traditional sequence of refinement-based correctness-preserving transformations starting from specification R by a sequence of relative correctness-based correctness-enhancing transformations starting from abort.
The traditional stepwise refinement based program derivation methodologies are primarily top-down. Strictly following the top-down program derivation approach may require backtracking resulting in rework. Moreover, th...
详细信息
ISBN:
(纸本)9783319274362;9783319274355
The traditional stepwise refinement based program derivation methodologies are primarily top-down. Strictly following the top-down program derivation approach may require backtracking resulting in rework. Moreover, the top down approach does not directly help in suggesting the next course of action in case of a failed derivation attempt. In this work we seamlessly incorporate a bottom up assumption propagation technique into a primarily top down derivation methodology. We present new tactics for back-propagating the assumptions made during the top-down phase. These tactics help in reducing the guesswork during the derivations. We have implemented these tactics in a program derivation system. With the help of simple examples, we show how this approach is useful for avoiding backtracking thereby simplifying the derivations.
We investigate the problem of finding a computable witness for the existential quantifier in a formula of the classical first-order predicate logic. The A-resolution calculus which is essentially the same as the progr...
详细信息
We investigate the problem of finding a computable witness for the existential quantifier in a formula of the classical first-order predicate logic. The A-resolution calculus which is essentially the same as the program derivation algorithm A of C.-***, R.C.-*** and *** is used for finding a definite substitution t for an existentially bound variable y in some formula F, such that F{t/y} is provable. The term t is built of the function and predicate symbols in F, plus Boolean functions and a case splitting function if, defined in the standard way: if (True, x, y) = x and if (False, x, y) = y. We prove that the A-resolution calculus is complete in the following sense: if such a definite substitution exists, then the A-calculus derives a clause giving such a substitution. The result is strengthened by allowing the usage of liftable criteria R of a certain type, prohibiting the derivation of the substitution terms t for which R(t) fails. This enables us to specify, for example, that the substitution t must be in some special signature or must be type-correct, without losing completeness. We will also consider ordering restrictions for the A-calculus.
A constructive method of program development is presented. It is based on a simple strategy for problem decomposition that is claimed to be more supportive of goal-oriented programming than the Wirth-Dijkstra top-down...
详细信息
A constructive method of program development is presented. It is based on a simple strategy for problem decomposition that is claimed to be more supportive of goal-oriented programming than the Wirth-Dijkstra top-down refinement method. With the proposed method, a program is developed by making a sequence of refinements, each of which can establish the postcondition for a corresponding sequence of progressively weaker preconditions until a mechanism has been composed that will establish the postcondition for the original given precondition for the problem. The strategy can minimize case analysis, simplify constructive program proofs, and ensure a correspondence between program structure and data structure. [ABSTRACT FROM AUTHOR]
Probabilistic predicates generalize standard predicates over a state space;with probabilistic predicate transformers one thus reasons about imperative programs in terms of probabilistic pre- and postconditions. Probab...
详细信息
Probabilistic predicates generalize standard predicates over a state space;with probabilistic predicate transformers one thus reasons about imperative programs in terms of probabilistic pre- and postconditions. Probabilistic healthiness conditions generalize the standard ones, characterizing ''real'' probabilistic programs, and are based on a connection with an underlying relational model for probabilistic execution;in both contexts demonic nondeterminism coexists with probabilistic choice. With the healthiness conditions, the associated weakest-precondition calculus seems suitable for exploring the rigorous derivation of small probabilistic programs.
This paper describes the automatic derivation of compiled patterns and of a pattern compiler by partial evaluation. Compiling a pattern is achieved by specializing a pattern matching program with respect to the patter...
详细信息
This paper describes the automatic derivation of compiled patterns and of a pattern compiler by partial evaluation. Compiling a pattern is achieved by specializing a pattern matching program with respect to the pattern. Generating a pattern compiler is achieved by specializing the specializer with respect to the pattern matching program, i.e., by self-application of the specializer. The compiled patterns and the compiler are semantics-based because they are obtained using meaning-preserving transformations upon the definitional pattern matching program and the partial evaluator. The results are unexpectedly good: not only all are the operations depending on the pattern (syntax analysis, resolution of cross-references due to the nonlinearity) performed at compile time, but whereas the general pattern matcher builds the substitution environment incrementally and for nothing in case of failure, compiled patterns perform all the structural and equality tests first, and build the result only if the match succeeds. This nontrivial runtime staging has been obtained automatically, which is remarkable because staging in general is known to be an art. This example stresses continuation-passing style as a convenient style for writing general programs. This style makes it possible to circumvent the approximations of binding time analysis (which is an essential requirement for efficient self-application), and in addition, to stage residual programs automatically. These observations have been confirmed by later experiments.
We combine relational algebra and program derivation methodology and reconstruct a proof of Richardson's theorem that every finite directed graph without circuits of odd length has a kernel as a relational program...
详细信息
We combine relational algebra and program derivation methodology and reconstruct a proof of Richardson's theorem that every finite directed graph without circuits of odd length has a kernel as a relational program. Also a generalization of the approach is presented. (C) 2000 Elsevier Science B.V. All rights reserved.
暂无评论