Error flow analysis of a computer program derives information about how potential data state errors may arise and propagate as the program executes. This information can be used to measure the semantic effects on an e...
详细信息
Error flow analysis of a computer program derives information about how potential data state errors may arise and propagate as the program executes. This information can be used to measure the semantic effects on an execution path caused by changing statements along the path. A dynamic style of error flow analysis is defined and a system for performing this analysis called Dynamic Error Flow Analysis (DEFA) is described. Examples of several semantic metrics produced by running DEFA are given.
We present a simple, practical algorithm for higher-order matching in the context of automatic program transformation. Our algorithm finds more matches than the standard second order matching algorithm of Huet and Lan...
详细信息
We present a simple, practical algorithm for higher-order matching in the context of automatic program transformation. Our algorithm finds more matches than the standard second order matching algorithm of Huet and Lang, but it has an equally simple specification, and it is better suited to the transformation of programs in modern programming languages such as Haskell or ML. The algorithm has been implemented as part of the MAG system for transforming functional programs. (C) 2001 Elsevier Science B.V. All rights reserved.
A recent interesting paper by Melton et al. [1] discussed finding measures which preserve intuitive orderings on software documents. Informally, if less-than-or-equal-to is such an ordering, then they argue that a mea...
详细信息
A recent interesting paper by Melton et al. [1] discussed finding measures which preserve intuitive orderings on software documents. Informally, if less-than-or-equal-to is such an ordering, then they argue that a measure M is a real-valued function defined on documents such that M(F) less-than-or-equal-to M(F) whenever F less-than-or-equal-to F'. However, in measurement theory, this is only a necessary condition for a measure M. The representation condition for measurement additionally requires the converse;that F less-than-or-equal-to F' whenever M(F) less-than-or-equal-to M(F). Using the measurement theory definition of a measure, we show that Melton et al.'s examples, like McCabe's cyclomatic complexity [2], are not measures of the proposed intuitive document ordering after all. However, by dropping the restriction to real-valued functions, we show that it is possible to define a measure which characterises Melton et al.'s order relation;this provides a considerable strengthening of the results in Reference 1. More generally, we show that there is no single real-valued measure which can characterise any intuitive notion of 'complexity' of programs. The power of measurement theory is further illustrated in a critical analysis of some recent work by Weyuker 131 et al. on axioms for software complexity measures.
The implementation of syntax-driven static semantic analysis of languages presenting recursive forward references in their definition requires the handling of a syntax tree. When dealing with languages for which the s...
详细信息
The implementation of syntax-driven static semantic analysis of languages presenting recursive forward references in their definition requires the handling of a syntax tree. When dealing with languages for which the syntax tree approach is very heavy to implement, a source code reorganisation operation may solve the problem more conveniently. This applies to the ISO specification language LOTOS [1, 2], which is ta ken as the main concern in the paper. The implementation is described of a static semantic analyser for LOTOS based on the above approach, by means of a C program, and all the main issues are addressed. It is shown that the source code reorganisation operation applied to LOTOS specifications does not alter the semantics of the original source specification. Examples and measures of performance collected by testing the tool on some significant case studies in the literature are also given.
Ming-Hua Zhang (1988) has proposed a new specification method for data types based on second-order logic. Now we show that errors and exceptions are included directly in the specifications from the beginning. In our a...
详细信息
Ming-Hua Zhang (1988) has proposed a new specification method for data types based on second-order logic. Now we show that errors and exceptions are included directly in the specifications from the beginning. In our approach errors are not objects but indicate that some formulas are false. Unlike errors, exceptions are special objects. The error, error propagation, error recovery and exception can all be precisely defined and the fundamental results about them can be deduced from the specification by predicate calculus.
The notion of reductivity of a relation with respect to a datatype is introduced and related to inductivity and initiality. The use of reductivity in constructing terminating programs is discussed. A calculus of reduc...
详细信息
The notion of reductivity of a relation with respect to a datatype is introduced and related to inductivity and initiality. The use of reductivity in constructing terminating programs is discussed. A calculus of reductivity, discussed in more detail in a companion paper, is introduced.
The lambda sigma -calculus is a concrete lambda -calculus of explicit substitutions, designed for reasoning about implementations of lambda -calculi. Higher-order abstract syntax is an approach to metaprogramming that...
详细信息
The lambda sigma -calculus is a concrete lambda -calculus of explicit substitutions, designed for reasoning about implementations of lambda -calculi. Higher-order abstract syntax is an approach to metaprogramming that explicitly captures the variable-binding aspects of programming language constructs. A new calculus of explicit substitutions for higher-order abstract syntax is introduced, allowing a high-level description of variable binding in object languages while also providing substitutions as explicit programmer-manipulable data objects. The new calculus is termed the lambda sigma beta (0)-calculus, since it makes essential use of an extension of beta (0)-unification (described in another paper). Termination and confluence are verified for the lambda sigma beta (0)-calculus similarly to that for the ncr-calculus, and an efficient implementation is given in terms of first-order renaming substitutions. The verification of confluence makes use of a verified adaptation of Nipkow's higher-order critical pairs lemma to the forms of rewrite rules required for the statement of the lambda sigma beta (0)-calculus. (C) 2001 Academic Press.
One of the design aims of Ada was to provide a language which would encourage the production of reliable programs: An important technique used to provide greater reliability is program verification. In this paper, we ...
详细信息
One of the design aims of Ada was to provide a language which would encourage the production of reliable programs: An important technique used to provide greater reliability is program verification. In this paper, we comment on the design of Ada from this particular point of view and we indicate particular approaches to the verification of Ada programs.
We investigate here the question of finding the minimal requirements for the registers used by n processes that solve the critical-section problem. For two processes, we show that there cannot be a solution to the cri...
详细信息
We investigate here the question of finding the minimal requirements for the registers used by n processes that solve the critical-section problem. For two processes, we show that there cannot be a solution to the critical-section problem if the two registers used are regular and of size 2 and 3. For n processes, this result generalizes to show the impossibility of a solution with regular registers if the total size of the registers is 3n - 1. This is the best result for n = 2 since there are solutions (presented here) in which regular registers of total size 6 are used. The impossibility proof depends on a careful analysis of infinite protocol automata, and therefore a detailed definition of such automata and their semantics is developed first.
In unrestricted branching programs all variables may be tested arbitrarily often on each path. But exponential lower bounds are only known if on each path the number of tests of each variable is bounded. We examine br...
详细信息
In unrestricted branching programs all variables may be tested arbitrarily often on each path. But exponential lower bounds are only known if on each path the number of tests of each variable is bounded. We examine branching programs in which for each path the number of variables that are tested more than once is bounded by k but we do not bound the number of tests of those variables. Using a new lower bound method we can prove that such branching programs become more powerful by increasing k only by 1: For k less than or equal to (1 - epsilon)(n/3)((1/3))/1og(2/3) n, where epsilon > 0, we exhibit Boolean functions that can be represented in polynomial size if k variables may be tested more than once on each path, but only in exponential size if k - 1 variables may be tested more than once on each path. Therefore, we obtain a tight hierarchy. (C) 1996 Academic Press, Inc.
暂无评论