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

A language-independent proof system for full program equivalence

FORMAL ASPECTS OF COMPUTING 2016年第3期28卷 469-497页

作者： Ciobaca, Stefan Lucanu, Dorel Rusu, Vlad Rosu, Grigore Alexandru Ioan Cuza Univ Fac Comp Sci 16 Gen Berthelot St Iasi 700483 Romania Inria Lille France Univ Illinois Champaign IL USA

Two programs are fully equivalent if, for the same input, either they both diverge or they both terminate with the same result. Full equivalence is an adequate notion of equivalence for programs written in deterministic languages. It is useful in many contexts, such as capturing the correctness of program transformations within the same language, or capturing the correctness of compilers between two different languages. In this paper we introduce a language-independent proof system for full equivalence, which is parametric in the operational semantics of two languages and in a state-similarity relation. The proof system is sound: a proof tree establishes the full equivalence of the programs given to it as input. We illustrate it on two programs in two different languages (an imperative one and a functional one), that both compute the Collatz sequence. The Collatz sequence is an interesting case study since it is not known whether the sequence terminates or not;nevertheless, our proof system shows that the two programs are fully equivalent (even if we cannot establish termination or divergence of either one).

关键词： Matching logic programming language semantics Program equivalence Full equivalence programming language aggregation

来源：评论

学校读者我要写书评

暂无评论

Compositional execution semantics for business process verification

引用

JOURNAL OF SYSTEMS AND SOFTWARE 2018年 137卷 217-238页

作者： Stachtiari, Emmanouela Katsaros, Panagiotis Aristotle Univ Thessaloniki Dept Informat Thessaloniki Greece

Service compositions are programmed as executable business processes in languages like WS-BPEL (or BPEL in short). In such programs, activities are nested within concurrency, isolation, compensation and event handling constructs that cause an overwhelming number of execution paths. Program correctness has to be verified based on a formal definition of the language semantics. For BPEL, previous works have proposed execution semantics in formal languages amenable to model checking. Most of the times the service composition structure is not preserved in the formal model, which impedes tracing the verification findings in the original program. Here, we propose a compositional semantics and a structure preserving translator of BPEL programs onto the BIP component framework. In addition, we verify essential correctness properties that affect process responsiveness, and the compliance with partner services. The scalability of the proposed translation and analysis is demonstrated on BPEL programs of various sizes. Our compositional translation approach can be also applied to other executable languages with nesting syntax. (C) 2017 Published by Elsevier Inc.

关键词： Formal verification programming language semantics WS-BPEL BIP

来源：评论

学校读者我要写书评

暂无评论

Integrating semantic and syntactic descriptions to chain geographic services

引用

IEEE INTERNET COMPUTING 2006年第5期10卷 42-52页

作者： Lemmens, Rob Wytzisk, Andreas de By, Rolf Granell, Carlos Gould, Michael Univ Jaume 1 Castellon Spain Delft Univ Technol Delft Netherlands

Integrating multiple geographic services from different information communities and spatiolinguistic regions is challenging because of its inherent complexity and heterogeneity. A geographic information systems workflow approach can use semantic and syntactic service descriptions to form service chains that can integrate service discovery, composition, and reuse. Service chaining links remote geographic services to help expert users form complex geoprocessing services and perform timely analysis of geodata. This method facilitates the use of XML-based service description languages to build a geoservice-reuse architecture based on common ontologies and shared service descriptions.

关键词： Geographic Information Systems Internet Ontologies Artificial Intelligence programming language semantics Software Architecture Software Reusability XML Semantic Description Syntactic Description Geographic Service Information Community Spatiolinguistic Region Geographic Information System Service Discovery Geoprocessing Service XML Based Service Description language Geoservice Reuse Architecture Geographic Information Systems Concrete Data Visualization Joining Processes Geoscience Information Analysis Performance Analysis Ontologies Web Services Production Facilities Semantic Annotation Service Reuse Geographic Services Description Discovery And Composition Methodology

来源：评论

学校读者我要写书评

暂无评论

External and internal choice with event groups in Event-B

引用

FORMAL ASPECTS OF COMPUTING 2012年第4-6期24卷 555-567页

作者： Butler, Michael Univ Southampton Southampton Hants England

Abrial's Event-B formalism for refinement-based system development is influenced by Back's action system approach. Morgan has defined a CSP-like failures-divergence semantics for action systems that distinguishes internal and external choice of actions. Morgan's semantics has the characteristic that the choice between enabled actions is external while internal choice is represented less directly through nondeterministic effect of actions. Practical experience with Event-B has demonstrated the need to be able to represent both internal and external choice between enabled events more explicitly. In this paper, Morgan's failures semantics for action systems is modified to allow both internal and external choice to be represented directly. This is achieved by grouping events so that external choice is between event groups and internal choice is within event groups. This leads to a refinement rule for preservation of choice between event groups while allowing for reduction of choice within event groups. We also provide a refinement rule for splitting event groups in order to increase external choice. The refinement rules are justified in terms of failures refinement.

关键词： programming language semantics THEOREMS (Mathematics) COMPUTER science PARAMETER estimation SEMANTIC integration (Computer systems)

来源：评论

学校读者我要写书评

暂无评论

A denotational semantics for continuous queries over streams and relations

引用

SIGMOD RECORD 2004年第3期33卷 6-11页

作者： Arasu, A Widom, J Stanford Univ Stanford CA 94305 USA

We specified a complete formal semantics for a generic continuous query language over streams and relations. Our semantics resolves any ambiguities present in informal language descriptions-it assigns an exact meaning to any query in the language, at any point in time, for any possible input streams and relations. Our generic language is built from a number of "black box" operators, whose semantics must be instantiated for a specific concrete language. As examples we instantiated a portion of CQL [ABW03], a language that includes SQL constructs, sliding windows over streams, and special-purpose relation-to-stream operators. In addition to clarifying the potentially subtle meaning of continuous queries, our formal semantics provides a tool for discovering and reasoning about equivalences within a given continuous query language, and for comparing expressiveness across different proposed languages.

关键词： programming language semantics Exploration semiotics semantics data base language SQL rivers streams language Reasoning

来源：评论

学校读者我要写书评

暂无评论

Comparative trace semantics of time Petri nets

引用

programming AND COMPUTER SOFTWARE 2015年第3期41卷 131-139页

作者： Bushin, D. I. Virbitskaite, I. B. Russian Acad Sci Siberian Div AP Ershov Inst Informat Syst Novosibirsk 630090 Russia Novosibirsk State Univ Novosibirsk 630090 Russia

In the paper, a family of trace equivalencies in the interleaving, step, partial order, and nondeterministic semantics is defined and studied in the context of time Petri nets. The equivalences studied are based both on the classical concept of transition firing sequences and on time processes, i.e., time extensions of net processes with global transition firing moments. Relationships between the equivalences are established, and a hierarchy of classes of equivalent time Petri nets is constructed.

关键词： programming language semantics PETRI nets EQUIVALENCE (Mathematics) ISOMORPHISMS (Mathematics) SEQUENCES (Mathematics)

来源：评论

学校读者我要写书评

暂无评论

Understanding programming languages

引用

MINDS AND MACHINES 2007年第2期17卷 203-216页

作者： Turner, Raymond Univ Essex Dept Comp Sci Colchester CO4 3SQ Essex England

We document the influence on programming language semantics of the Platonism/formalism divide in the philosophy of mathematics.

关键词： programming language semantics operational denotational

来源：评论

学校读者我要写书评

暂无评论

Regression test selection using class, sequence and activity diagrams

引用

IET SOFTWARE 2016年第3期10卷 72-80页

作者： Dahiya, Sumit Bhatia, Rajesh K. Rattan, Dhavleesh Deenbandhu Chhotu Ram Univ Sci & Technol Comp Sci & Engn Dept Sonipat Haryana India PEC Univ Technol Dept Comp Sci & Engn Chandigarh 160012 India Punjabi Univ Dept Comp Engn Patiala Punjab India

Regression test selection is a process to select a subset of existing test cases, which are then used with some new test cases for regression testing. Regression testing ensures that the changes made to the system have not affected the existing functionality. To date, there is no adequate technique which can do regression test selection by considering changes in semantics of operations (along with the other syntax and semantics changes) using UML diagrams. Change in semantics of an operation refers to the change in conditional statements, change in independent paths/unique paths, change in control flow and addition or deletion of any content from the existing functionality. In this study, a novel approach is presented which can do this using class, sequence and activity diagrams. The tool compared old and new versions of UML diagrams to categorise test cases into reusable, retestable, obsolete and newly generated category. Activity diagrams are specifically used to test the semantics of operations. The changed operations corresponding to these activity diagrams are also searched in class and sequence diagrams for regression test selection. This study has been validated by comparison with previous study. It is found that the authors' work provides significant increase in accuracy.

关键词： programming language semantics Unified Modeling language program testing software reusability regression test selection activity diagrams subset selection operations semantics UML diagrams conditional statements independent paths unique paths control flow class sequence reusable test case retestable test case obsolete test cases new test case generation algorithm

来源：评论

学校读者我要写书评

暂无评论

Automatic differentiation for ML-family languages: Correctness via logical relations

引用

MATHEMATICAL STRUCTURES IN COMPUTER SCIENCE 2024年第8期34卷 747-806页

作者： Nunes, Fernando Lucatelli Vakar, Matthijs Univ Utrecht Dept Informat & Comp Sci Utrecht Netherlands Univ Coimbra Dept Math CMUC Coimbra Portugal

We give a simple, direct, and reusable logical relations technique for languages with term and type recursion and partially defined differentiable functions. We demonstrate it by working out the case of automatic differentiation (AD) correctness: namely, we present a correctness proof of a dual numbers style AD code transformation for realistic functional languages in the ML-family. We also show how this code transformation provides us with correct forward- and reverse-mode *** starting point is to interpret a functional programming language as a suitable freely generated categorical structure. In this setting, by the universal property of the syntactic categorical structure, the dual numbers AD code transformation and the basic $\boldsymbol{\omega } \mathbf{Cpo}$ -semantics arise as structure preserving functors. The proof follows, then, by a novel logical relations *** key to much of our contribution is a powerful monadic logical relations technique for term recursion and recursive types. It provides us with a semantic correctness proof based on a simple approach for denotational semantics, making use only of the very basic concrete model of $\omega$ -cpos.

关键词： programming language semantics Differentiable programming languages Recursive types Logical relations Program transformations Software correctness

来源：评论

学校读者我要写书评

暂无评论

A procedure-oriented generic bill of materials

引用

COMPUTERS & INDUSTRIAL ENGINEERING 1997年第1期32卷 29-45页

作者： Olsen, KA Saetre, P Thorstenson, A RES CTR MOLDE N-6400 MOLDENORWAY

Bill of Materials (BOM) structures describe the component structure of a product, most often as a tabular structure implemented within a relational database system. The conventional approach is to design a unique BOM for each model or variant of a product. This becomes impossible with a customer-oriented production, where the number of variants may go into high numbers. The solution is to describe and maintain one generic structure that encompasses all variants of a product. This structure may then be used to generate a BOM for each particular variant. Earlier attempts to develop a generic BOM system have been directed towards improving the conventional tabular structures. These efforts have several limitations, mainly because the tabular structure does not offer the flexibility needed to describe generic structures. We propose a generic structure based on a programming language notation. This notation makes it possible to describe the set of possible variants of a product by handling both functional and structural relations between components. The user can explode (execute) any part of the BOM to define a specific product variant. User specifications are given dynamically, as the generic BOM is executed. The system will then automatically generate a specific BOM for this particular product variant. A prototype system has been developed. Copyright (C) 1997 Elsevier Science Ltd

关键词： Industrial management Bills of particulars programming language semantics

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：