We develop an explicit two level system that allows programmers to reason about the behavior of effectful programs. the first level is an ordinary ML-style type system, which confers standard properties on program beh...
详细信息
ISBN:
(纸本)9781581137569
We develop an explicit two level system that allows programmers to reason about the behavior of effectful programs. the first level is an ordinary ML-style type system, which confers standard properties on program behavior. the second level is a conservative extension of the first that uses a logic of type refinements to check more precise properties of program behavior. Our logic is a fragment of intuitionistic linear logic, which gives programmers the ability to reason locally about changes of program state. We provide a generic resource semantics for our logic as well as a sound, decidable, syntactic refinement-checking system. We also prove that refinements give rise to an optimization principle for programs. Finally, we illustrate the power of our system through a number of examples.
We define (set-theoretic) notions of intensional Henkin model and syntactic lambda-algebra for Moggi's partial lambda-calculus. these models are shown to be equivalent to the originally described categorical model...
详细信息
ISBN:
(纸本)3540408010
We define (set-theoretic) notions of intensional Henkin model and syntactic lambda-algebra for Moggi's partial lambda-calculus. these models are shown to be equivalent to the originally described categorical models via the global element construction;the proof makes use of a previously introduced construction of classifying categories. the set-theoretic semantics thus obtained is the foundation of the higher order algebraic specification language HASCASL, which combines specification and functional programming.
this paper starts from a denotational semantics for first order logic proposed by Apt. He interprets first order logic as a programming language within the declarative paradigm, but different from the usual approach o...
详细信息
Protocols for distributed systems make often use of random transitions to achieve a common goal. A popular example are randomized leader election protocols. We introduce probabilistic product automata (PPA) as a natur...
详细信息
ISBN:
(纸本)3540206329
Protocols for distributed systems make often use of random transitions to achieve a common goal. A popular example are randomized leader election protocols. We introduce probabilistic product automata (PPA) as a natural model for this kind of systems. To reason about these systems, we propose to use a product version of linear temporal logic (LTLcircle times). the main result of the paper is a model-checking procedure for PPA and LTLcircle times. With its help, it is possible to check qualitative properties of distributed systems automatically.
Traditional approaches to object-oriented style emphasize classes with a basic set of constructors and a minimal set of methods that when combined permit the full potential of the instance objects to be realized. this...
详细信息
ISBN:
(纸本)1581136722
Traditional approaches to object-oriented style emphasize classes with a basic set of constructors and a minimal set of methods that when combined permit the full potential of the instance objects to be realized. this object-oriented style is probably modeled on the style used in mathematics and logic to develop a system based on a minimal set of axioms and operations. the consequences of this style both in practice and in pedagogy are that objects enter into existence in an embryonic state and must be nurtured to maturity by a sequence of method calls that tweak behavior and/or add data. Although this minimalist approach is useful in the first stages of teaching objects and in exploratory design, we suggest that most designs should evolve towards building classes with a rich set of constructors and methods so that the instance objects may be born mature, that is, ready to use in the program without further tweaking. In particular, we believe that if students are taught to design in this manner, then they will be more effective both as students and as computing professionals. the ideas in this article have developed from our experience in designing the Java Power Tools (JPT) and in applying these tools to build many labs and demo programs. We found that using the traditional minimalist design approach hindered our ability to rapidly develop interesting applications. Gradually, we evolved boththe tools and the examples to be far richer and have found that our development time has been dramatically reduced. We believe that those who teach objects may be interested in these principles even if they choose to work with entirely different tools and examples.
Action refinement is a practical hierarchical method to ease the design of large reactive systems. Relating hierarchical specification to hierarchical implementation is an effective method to decrease the complexity o...
详细信息
ISBN:
(纸本)3540206329
Action refinement is a practical hierarchical method to ease the design of large reactive systems. Relating hierarchical specification to hierarchical implementation is an effective method to decrease the complexity of the verification of these systems. In our previous work [15], this issue has been investigated in the simple case of the refinement of an action by a finite process. In this paper, on the one hand, we extend our previous results by considering the issue in general, i.e., refining : an abstract action by an arbitrary process;on the other hand, we exploit different techniques such that our method is easier to be followed and applied in practice.
During a course on computer architecture, assembler, C programming, network and communication, 57 out of 300 students were followed closely by questionnaires and tests in order to evaluate their learning of computer a...
详细信息
ISBN:
(纸本)9781581136722
During a course on computer architecture, assembler, C programming, network and communication, 57 out of 300 students were followed closely by questionnaires and tests in order to evaluate their learning of computer architecture. the results indicate boththat the students' understanding of logic gates and Boolean algebra is poorer than preferred, and that the students also have difficulties grasping the implementation of higher level constructs in low level architecture features. Better results might have been achieved if the teaching of architecture was closely linked to the students' previous training in programming.
Recently, planning based on answer set programming has been proposed as an approach towards realizing declarative planning systems. In this paper, we present the language K-c, which extends the declarative planning la...
详细信息
Recently, planning based on answer set programming has been proposed as an approach towards realizing declarative planning systems. In this paper, we present the language K-c, which extends the declarative planning language K by action costs. K-c provides the notion of admissible and optimal plans, which are plans whose overall action costs are within a given limit resp. minimum over all plans (i.e., cheapest plans). As we demonstrate, this novel language allows for expressing some nontrivial planning tasks in a declarative way. Furthermore, it can be utilized for representing planning problems under other optimality criteria, such as computing "shortest" plans (withthe least number of steps), and refinement combinations of cheapest and fastest plans. We study complexity aspects of the language K-c and provide a transformation to logic programs, such that planning problems are solved via answer set programming. Furthermore, we report experimental results on selected problems. Our experience is encouraging that answer set planning may be a valuable approach to expressive planning systems in which intricate planning problems can be naturally specified and solved.
We propose a framework which extends Antitonic logic Programs [2] to an arbitrary complete bilattice of truth-values, where belief and doubt are explicitly represented. Based on Fitting's ideas, this framework all...
详细信息
ISBN:
(纸本)3540441905
We propose a framework which extends Antitonic logic Programs [2] to an arbitrary complete bilattice of truth-values, where belief and doubt are explicitly represented. Based on Fitting's ideas, this framework allows a precise definition of important operators found in logicprogramming such as explicit negation and the default negation. In particular, it leads to a natural integration of explicit negation withthe default negation through the coherence principle [19]. According to this principle, the explicit negation entails the default negation. We then define Coherent Answer Sets, and the Paraconsistent Well-founded Model semantics, generalizing paraconsistent semantics for logic program (for instance, WFSXp [4]). Our framework is an extension of important classes of Antitonic logic Programs, and is general enough to capture Probabilistic Deductive Databases, Possibilistic logicprogramming, Hybrid Probabilistic logic Programs, and Fuzzy logicprogramming. thus, we have a powerful mathematical formalism for dealing with default reasoning, paraconsistency, and uncertainty.
this paper presents a new logicprogramming language for modelling Agents and Multi-Agent systems in computational logic. the basic objective of the specification of this new language has been the identification and t...
详细信息
ISBN:
(纸本)3540441905
this paper presents a new logicprogramming language for modelling Agents and Multi-Agent systems in computational logic. the basic objective of the specification of this new language has been the identification and the formalization of what we consider to be the basic patterns for reactivity, proactivity, internal "thinking", and "memory". the formalization models these concepts by introducing different kinds of events, with a suitable treatment. We introduce a novel approach to the language semantics, called the evolutionary semantics.
暂无评论