In this paper, we explore the testing-verification relations-hip withthe objective of mechanizing the generation of test data. We consider program classes defined as recursive program schemes and we show that complet...
详细信息
In component-based software development, object-oriented design (OOD) frameworks are increasingly recognised as better units of reuse than objects. this is because OOD frameworks are groups of interacting objects, and...
详细信息
Schema-basedprogramsynthesis and transformation techniques tend to be either pragmatic, designed for carrying out real programtransformation or synthesis operations but lacking the logical basis to ensure correctne...
ISBN:
(数字)9783540489580
ISBN:
(纸本)3540657657
Schema-basedprogramsynthesis and transformation techniques tend to be either pragmatic, designed for carrying out real programtransformation or synthesis operations but lacking the logical basis to ensure correctness of the programs they synthesise/transform, or rigorous, with strong theoretical foundations, but generating proof obligations which are difficult to satisfy.
In this paper we present a program specialisation method which, given a call/post specification, transforms a logicprogram into a weakly call-correct one satisfying the post-condition. the specialisation is applied t...
详细信息
ISBN:
(数字)9783540489580
ISBN:
(纸本)3540657657
In this paper we present a program specialisation method which, given a call/post specification, transforms a logicprogram into a weakly call-correct one satisfying the post-condition. the specialisation is applied to specialised partially correct programs. this notion is based on the definition of specialised derivation which is intended to describe program behaviour whenever some properties on procedure calls are assumed. Top-down and bottom-up semantics of specialised derivations are recalled.
this paper presents an automated method that deals with termination of constraint logicprograms in two steps. First, from the text of a program, the method infers a set of potentially terminating classes using abstra...
详细信息
ISBN:
(数字)9783540489580
ISBN:
(纸本)3540657657
this paper presents an automated method that deals with termination of constraint logicprograms in two steps. First, from the text of a program, the method infers a set of potentially terminating classes using abstract interpretation and boolean mu-calculus. By "potentially", we roughly mean that for each of these classes, one can find a static order over the literals of the clauses of the program to ensure termination. then, given a terminating class among those computed at the first step, the second step consists of a "compilation" (or transformation) of the original program to another one by reordering literals. For this new program, the universal left-termination of any query of the considered class is guaranteed. the method has been implemented.
Well-quasi orders in general, and homeomorphic embedding in particular, have gained popularity to ensure online termination of program analysis, specialisation and transformation techniques. It has been recently shown...
详细信息
ISBN:
(数字)9783540489580
ISBN:
(纸本)3540657657
Well-quasi orders in general, and homeomorphic embedding in particular, have gained popularity to ensure online termination of program analysis, specialisation and transformation techniques. It has been recently shown that the homeomorphic embedding relation is strictly more powerful than a large class of involved well-founded approaches. In this paper we provide some additional investigations on the power of homeomorphic embedding. We, however, also illustrate that the homeomorphic embedding relation suffers from several inadequacies in contexts where logical variables arise. We therefore present new, extended homeomorphic embedding relations to remedy this problem.
this paper describes a class of decision procedures that we have found useful for efficient, domain-specific deductive synthesis, and a method for integrating this type of procedure into a general-purpose refutation-b...
详细信息
ISBN:
(纸本)3540657657
this paper describes a class of decision procedures that we have found useful for efficient, domain-specific deductive synthesis, and a method for integrating this type of procedure into a general-purpose refutation-basedtheorem prover. We suggest that this is a large and interesting class of procedures and show how to integrate these procedures to accelerate a general-purpose theorem prover doing deductive synthesis. While much existing research on decision procedures has been either in isolation or in the context of interfacing procedures to non-refutation-basedtheorem provers, this appears to be the first reported work on decision procedures in the context of refutation-based deductive synthesis where witnesses must be found.
the Ω logic, is designed to specify, to reason about and to synthesize imperative programs in an object oriented language, namely C++. there exists a lot of systems where computing-by-proof is possible but th...
ISBN:
(纸本)3540657657
the Ω logic, is designed to specify, to reason about and to synthesize imperative programs in an object oriented language, namely C++. there exists a lot of systems where computing-by-proof is possible but there are based on more or less classical logics and produce λ-expressions. We make the distinction between programming and computing. Functional programs are obviously in the second category. Even if imperative programs can be modeled with functions, thanks to denotational semantics, this is not realistic. We are interested in the first category: we want to synthesize programs doing actions.
this work is inspired by D.R. Smith’s research on synthesising global search (GS) programs (in the Refine language) from first-order logic specifications (also in Refine) [8,9,10]. We concentrate on synthesi...
ISBN:
(数字)9783540489580
ISBN:
(纸本)3540657657
this work is inspired by D.R. Smith’s research on synthesising global search (GS) programs (in the Refine language) from first-order logic specifications (also in Refine) [8,9,10]. We concentrate on synthesising constraint logicprograms (CLP) [6] instead. We thus only have to synthesise code that (incrementally) poses the constraints, because the actual constraint propagation and pruning are performed by the CLP system. We here only tackle the family of decision assignment problems; the families of optimisation assignment problems, decision permutation problems, and optimisation permutation problems are covered in [4].
暂无评论