检索结果-内蒙古大学图书馆

A FIXED-POINT THEOREM IN A CATEGORY OF COMPACT METRIC-SPACES

THEORETICAL COMPUTER SCIENCE 1995年第1-2期146卷 311-320页

作者： ALESSI, F BALDAN, P BELLE, G UNIV UDINE DIPARTIMENTO MATEMAT & INFORMAT VIA ZANON 6 I-33100 UDINE ITALY

Various results appear in the literature for deriving existence and uniqueness of fixed points for endofunctors on categories of complete metric spaces. All these results are proved for contracting functors which satisfy some further requirements, depending on the category in question. Following a new kind of approach, based on the notion of eta-isometry, we show that the sole hypothesis of contractivity is enough for proving existence and uniqueness of fixed points for endofunctors on the category of compact metric spaces and embedding-projection pairs.

关键词： Denotational semantics Domain equations Endofunctors Concurrency Uniqueness Concurrency metric space Category Fixed point programming language semantics uniqueness

来源：评论

学校读者我要写书评

暂无评论

Partial Order Reduction for Rewriting semantics of programming languages

引用

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2007年第4期176卷 61-78页

作者： Farzan, Azadeh Meseguer, Jose Univ Illinois Comp Sci Dept Urbana IL 61801 USA

Software model checkers are typically language-specific, require substantial development efforts, and are hard to reuse for other languages. Adding partial order reduction (POR) capabilities to such tools typically requires sophisticated changes to the tool's model checking algorithms. This paper proposes a new method to make software model checkers language-independent and improving their performance through POR. Getting the POR capabilities does not require making any changes to the underlying model checking algorithms: for each language L, they are instead achieved through a theory transformation RL(sic) RL+ POR of L's formal semantics, rewrite theory RL. Under very minimal assumptions, this can be done for any language L with relatively little effort. Our experiments with the JVM, a Promela-like language and Maude indicate that significant state space reductions and time speedups can be gained for tools generated this way.

关键词： Partial order reduction model checking programming language semantics rewriting logic Maude

来源：评论

学校读者我要写书评

暂无评论

The semantics of Metaprogramming in Prolog

引用

THEORY AND PRACTICE OF LOGIC programming 2024年第4期24卷 885-900页

作者： Warren, David scott SUNY Stony Brook Stony Brook NY 11794 USA XSB Inc Setauket NY USA

This paper describes a semantics for pure Prolog programs with negation that provides meaning to metaprograms. Metaprograms are programs that construct and use data structures as programs. In Prolog a primary mataprogramming construct is the use of a variable as a literal in the body of a clause. The traditional Prolog 3-line metainterpreter is another example of a metaprogram. The account given here also supplies a meaning for clauses that have a variable as head, even though most Prolog systems do not support such clauses. This semantics naturally includes such programs, giving them their intuitive meaning. Ideas from Denecker and his colleagues form the basis of this approach. The key idea is to notice that if we give meanings to all propositional programs and treat Prolog rules with variables as the set of their ground instances, then we can give meanings to all programs. We must treat Prolog rules (which may be metarules) as templates for generating ground propositional rules, and not as first-order formulas, which they may not be. We use parameterized inductive definitions to give propositional models to Prolog programs, in which the propositions are expressions. Then the set of expressions of a propositional model determine a first-order Herbrand Model, providing a first-order logical semantics for all (pure) Prolog programs, including metaprograms. We give examples to show the applicability of this theory. We also demonstrate how this theory makes proofs of some important properties of metaprograms very straightforward.

关键词： inductive definitions prolog semantics programming language semantics interpretation

来源：评论

学校读者我要写书评

暂无评论

Building Verification Condition Generators by Compositional Extension

引用

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2007年 191卷 73-83页

作者： van Leeuwen, A. J. Univ Utrecht Dept Informat & Comp Sci Utrecht Netherlands

Current mechanizations of programming logics are often in the form of verification condition generators. These front ends to a prover translate a program and assertions into conditions that state that the program fulfills its assertions. Traditional verification condition generators are monolithic encapsulations of a programming language's semantics. This makes it hard to build such verification generators when designing a new language, or when extending a language. We propose a more compositional method of building verification condition generators, using ideas from monadic denotational semantics and from generic programming. Our technique allows us to extend an existing verification condition generator to handle new language constructs, but also to add extensions at another level, such as the ability to generate validation traces. We explain the technique through an example, extending a simple while language with a construct for exception handling. This construct not only needs an extension to the logic, but also a change of its structure.

关键词： Hoare logic monadic logic programming language semantics

来源：评论

学校读者我要写书评

暂无评论

MATHEMATICAL PRINCIPLES FOR A 1ST COURSE IN SOFTWARE ENGINEERING

引用

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING 1989年第5期15卷 550-559页

作者： MILLS, HD BASILI, VR GANNON, JD HAMLET, RG UNIV MARYLAND DEPT COMP SCI COLLEGE PK MD 20742 USA PORTLAND STATE UNIV DEPT COMP SCI PORTLAND OR 97207 USA UNIV MARYLAND INST ADV COMP STUDIES COLLEGE PK MD 20742 USA

The discipline of software engineering has transferred the commonsense methods of good programming and management to large software projects, it has been less successful in acquiring a solid theoretical foundation for these methods. We have developed an introductory computer science course, much as calculus is a basic course for mathematics and the physical sciences, concerned primarily with theoretical foundations and methodology rather than apprenticeship through applications. This paper describes the principles taught in the course and gives a small example illustrating them. [ABSTRACT FROM AUTHOR]

关键词： Index Terms-Formal specification program verification programming language semantics software development

来源：评论

学校读者我要写书评

暂无评论

RECURRENCE DOMAINS - THEIR UNIFICATION AND APPLICATION TO LOGIC programming

引用

INFORMATION AND COMPUTATION 1995年第1期122卷 45-69页

作者： CHEN, H HSIANG, J NATL TAIWAN UNIV DEPT COMP SCI TAIPEI 10764 TAIWAN SUNY STONY BROOK DEPT COMP SCI STONY BROOK NY 11794 USA

In this paper we present a formalism for finitely representing infinite sets of terms. This formalism, called rho-terms, enables us to reason finitely about certain recursive types. We present an extension of Horn logic programs, called rho-Prolog, which allows a finite schematization of infinitely many clauses via predicates with rho-terms as arguments. We show that for every rho-Prolog program there is an equivalent Horn logic program. That is, incorporating rho-terms into first order logic programming does not change its denotational semantics. Computationally, however, rho-Prolog has the advantages of (1) representing infinitely many answers finitely, (2) avoiding repetition in computation and thus achieving better efficiency, (3) allowing infinite queries, and (4) avoiding certain kinds of non-termination of Prolog programs. The rho-terms play a similar role to regular-trees and sort-expressions in explicitly defining abstract data types. It differs from the others in that it allows us to define certain non-regular-tree sets such as {(a(n), b(n), c(n)): n epsilon N}. We present a finite and complete algorithm for unification between rho-terms, with which we can also compute the intersections of the sets defined by rho-terms. (C) 1995 Academic Press, Inc.

关键词： abstract data types formalism Finite Predicate programming language semantics PROLOG Horns Logic programming Disputes infinite set Infinite SETTING

来源：评论

学校读者我要写书评

暂无评论

INDUCTIVE ATTRIBUTE GRAMMARS - A BASIS FOR INCREMENTAL PROGRAM EXECUTION

引用

ACTA INFORMATICA 1995年第2期32卷 117-144页

作者： WALZ, JA JOHNSON, GF Department of Computer Science University of Maryland College Park USA

Attribute grammars are traditionally constrained to be noncircular. In using attribute grammars to specify the semantics of programming languages, this noncircularity limitation has restricted attribute grammars to compile-time or static semantics. Inductive attribute grammars add a general form of circularity to this standard approach. Inductive attribute grammars have the expressiveness required to describe the full semantics of programming languages, while at the same time maintaining the declarative character of standard attribute grammars. This expanded view of attribute grammars proves to be useful in interactive language-based programming environments, as inductive attribute grammars allow the environment to provide an interpreter for incremental re-evaluation of programs after small changes to the code. The addition of run-time semantics via circular attribute grammars permits automatically generated environments to be complete, in that incremental static semantic checking and fast incremental execution are now available within a single framework.

关键词： programming language semantics semantics interpreters NON-CIRCULAR syntax Perspective drawings attribute grammars

来源：评论

学校读者我要写书评

暂无评论

HOL4P4: Mechanized Small-Step semantics for P4

引用

PROCEEDINGS OF THE ACM ON programming languageS-PACMPL 2024年第OOPSLA期8卷 223-249页

作者： Alshnakat, Anoud Lundberg, Didrik Guanciale, Roberto Dam, Mads KTH Royal Inst Technol Stockholm Sweden Saab AB Jarfalla Sweden

We present the first semantics of the network data plane programming language P4 able to adequately capture all key features of P4(16), the most recent version of P4, including external functions (externs) and concurrency. These features are intimately related since, in P4, extern invocations are the only points at which one execution thread can affect another. Reflecting P4's lack of a general-purpose memory and the presence of multithreading the semantics is given in small-step style and eschews the use of a heap. In addition to the P4 language itself, we provide an architectural level semantics, which allows the composition of P4-programmed blocks, models end-to-end packet processing, and can take into account features such as arbitration and packet recirculation. A corresponding type system is provided with attendant progress, preservation, and type-soundness theorems. semantics, type system, and meta-theory are formalized in the HOL4 theorem prover. From this formalization, we derive a HOL4 executable semantics that supports verified execution of programs with partially symbolic packets able to validate simple end-to-end program properties.

关键词： P4 programming language semantics interactive theorem proving formal verification

来源：评论

学校读者我要写书评

暂无评论

ALIASING AMONG POINTERS IN EUCLID

引用

INFORMATION PROCESSING LETTERS 1979年第2期9卷 76-79页

作者： SCHWARTZ, RL Department of Applied Mathematics Weizmann Institute of Science Rehovot Israel

来源：评论

学校读者我要写书评

暂无评论

Memory Representations in Rewriting Logic semantics Definitions

引用

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2009年第3期238卷 155-172页

作者： Hills, Mark Univ Illinois Dept Comp Sci Urbana IL 61801 USA

The executability of rewriting logic makes it a compelling environment for language design and experimentation;the ability to interpret programs directly in the language semantics develops assurance that definitions are correct and that language features work well together. However, this executability raises new questions about language semantics that don't necessarily make sense with non-executable definitions. For instance, suddenly the performance of the semantics, not just language interpreters or compilers based on the semantics, can be important, and representations must be chosen carefully to ensure that executing programs directly in language definitions is still feasible. Unfortunately, many obvious representations common in other semantic formalisms can lead to poor performance, including those used to represent program memory. This paper describes two different memory representations designed to improve performance: the first, which has been fully developed, is designed for use in imperative programs, while the second, still being developed, is intended for use in a variety of languages, with a special focus on pure object-oriented languages. Each representation is described and compared to the initial representation used in the language semantics, with thoughts on reuse also presented.

关键词： Rewriting logic programming language semantics performance

来源：评论

学校读者我要写书评

暂无评论

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

建议与咨询 留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案： 新增检索档案 确定 取消

请选择收藏分类： 新增自定义分类 确定 取消

通借通还

建议与咨询留下您的常用邮箱和电话号码，以便我们向您反馈解决方案和替代方法

请选择保存的检索档案：

请选择收藏分类：