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

A CRITICAL COMPARISON OF SEVERAL programming language implementationS

SOFTWARE-PRACTICE & EXPERIENCE 1980年第6期10卷 435-473页

作者： BOOM, HJ DEJONG, E Mathematisch Centrum Boerhaavestraat 49 1091 AL Amsterdam The Netherlands

AbstractThe implementations of Algol 60, FORTRAN, Pascal and Algol 68 provided on the CDC Cyber 73 of the Stichting Academisch Rekencentrum Amsterdam are compared on both qualitative and quantitative aspects. This paper concentrates on those aspects which are likely to be of interest to language designers and implementers, and to users of other computer systems.

关键词： Algol 60 FORTRAN Pascal Algol 68 programming language implementation CDC Cyber 73

来源：评论

学校读者我要写书评

暂无评论

Deep specification and proof preservation for the CoqTL transformation language

引用

SOFTWARE AND SYSTEMS MODELING 2022年第5期21卷 1831-1852页

作者： Cheng, Zheng Tisi, Massimo Univ Lorraine INRIA LORIA CNRS Nancy France IMT Atlantique LS2N UMR CNRS 6004 Nantes France

Executable engines for relational model-transformation languages evolve continuously because of language extension, performance improvement and bug fixes. While new versions generally change the engine semantics, end-users expect to get backward-compatibility guarantees, so that existing transformations do not need to be adapted at every engine update. The CoqTL model-transformation language allows users to define model transformations, theorems on their behavior and machine-checked proofs of these theorems in Coq. Backward-compatibility for CoqTL involves also the preservation of these proofs. However, proof preservation is challenging, as proofs are easily broken even by small refactorings of the code they verify. In this paper, we present the solution we designed for the evolution of CoqTL. We provide a deep specification of the transformation engine, including a set of theorems that must hold against the engine implementation. Then, at each milestone in the engine development, we certify the new version of the engine against this specification, by providing proofs of the impacted theorems. The certification formally guarantees end-users that all the proofs they write using the provided theorems will be preserved through engine updates. We illustrate the structure of the deep specification theorems, we produce a machine-checked certification of three versions of CoqTL against it, and we show examples of user proofs that leverage this specification and are thus preserved through the updates. Finally, we discuss the evolution of the deep specification by an extension mechanism, we present an evolution that introduces trace links in the specification, and we show which user proofs are preserved through specification evolutions.

关键词： MDE Model transformation programming language implementation Certification Theorem proving Coq

来源：评论

学校读者我要写书评

暂无评论

Quantifying and evaluating the space overhead for alternative C++ memory layouts

引用

SOFTWARE-PRACTICE & EXPERIENCE 2003年第7期33卷 595-636页

作者： Sweeney, PF Burke, M IBM Corp Thomas J Watson Res Ctr Yorktown Hts NY 10598 USA

This paper develops a formalism that precisely characterizes when class tables are required for C++ memory layouts. A memory layout is a particular choice of data structures for implementing run-time support for object-oriented languages. We use this formalism to quantify and evaluate, on a set of benchmarks, the space overhead for a set of C++ memory layouts. In particular, this paper studies the space overhead due to three language features: virtual dispatch, virtual inheritance, and dynamic typing. To date, there has been no scientific quantification or evaluation of C++ memory layouts. Our approach can help C++ implementors. This work has already influenced the memory layout design choices in IBM's Visual Age C++ V5 compiler. Applying our approach to a set of five benchmarks, we demonstrate that the impact of object-oriented space overhead can vary dramatically between applications (ranging from 0.42% to 99.79% for our benchmarks). In particular, applications whose object space is dominated by instances of classes that heavily use object-oriented language features will be significantly impacted by the choice of a memory layout. Copyright (C) 2003 John Wiley Sons, Ltd.

关键词： object-oriented optimizations programming language implementation C plus

来源：评论

学校读者我要写书评

暂无评论

Implementing Dynamic-Cut in TOY

引用

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2007年第1期177卷 153-168页

作者： Caballero, R. Garcia-Ruiz, Y. Univ Complutense Madrid Dept Sistemas Informati Programac Madrid Spain

This paper presents the integration of the optimization known as dynamic cut within the functional-logic system TOY. The implementation automatically detects deterministic functions at compile time, and includes in the generated code the test for detecting at run-time the computations that can actually be pruned. The outcome is a much better performance when executing deterministic functions including either or-branches in their definitional trees or extra variables in their conditions, with no serious overhead in the rest of the computations. The paper also proves the correctness of the criterion used for detecting deterministic functions w.r.t. the semantic calculus CRWL.

关键词： determinism functional-logic programming program analysis programming language implementation

来源：评论

学校读者我要写书评

暂无评论

RECURSIVE DATA STRUCTURES

引用

INTERNATIONAL JOURNAL OF COMPUTER & INFORMATION SCIENCES 1975年第2期4卷 105-132页

作者： HOARE, CAR QUEENS UNIV BELFAST DEPT COMP SCIBELFAST BT7 1NNNORTH IRELAND

The power and convenience of a programming language may be enhanced for certain applications by permitting treelike data structures to be defined by recursion. This paper suggests a pleasing notation by which such structures can be declared and processed; it gives the axioms which specify their properties, and suggests an efficient implementation method. It shows how a recursive data structure may be used to represent another data type, for example, a set. It then discusses two ways in which significant gains in efficiency can be made by selective updating of structures, and gives the relevant proof rules and hints for implementation. The examples show that a certain range of applications in symbol manipulation can be efficiently programmed without introducing the low-level concept of a reference into a high-level programming language.

关键词： axiomatic proof rules data representation Data structures dynamic storage allocation pointers (abolition of) programming language design programming language features programming language implementation recursive data structures references (abolition of) symbol manipulation

来源：评论

学校读者我要写书评

暂无评论

Free Objects in Constraint-logic Object-oriented programming 2021

Free Objects in Constraint-logic Object-oriented Programming

引用

23rd International Symposium on Principles and Practice of Declarative programming (PPDP)

作者： Dagefoerde, Jan C. Winkelmann, Hendrik Kuchen, Herbert Univ Munster ERCIS Munster Germany

ISBN: (纸本)9781450386890

Constraint-logic object-oriented programming facilitates the integrated development of business software that occasionally solves constraint-logic problems or makes other use of structured search. So far, work in constraint-logic object-oriented programming has been limited to considering constraints that only involve logic variables of primitive types;in particular, boolean, integer, and floating-point numbers. However, the availability of object-oriented features calls for the option to use logic variables in lieu of objects as well. Therefore, support for reference-type logic variables (or free objects) is required. With the work at hand, we add support for free objects to a Java-based constraint-logic object-oriented language, Muli. Allowing free objects in statements and expressions results in novel interactions with objects at run time, for instance, non-deterministic execution of polymorphic method invocations (taking arbitrary class hierarchies into account) and non-deterministic type operations. At run time, this is supported by a dynamic type constraint that restricts the possible types of a free object at non-deterministic choices.

关键词： Constraint-logic object-oriented programming reference-type logic variables programming language implementation runtime systems

来源：评论

学校读者我要写书评

暂无评论

Certifying a Rule-Based Model Transformation Engine for Proof Preservation 20

Certifying a Rule-Based Model Transformation Engine for Proo...

引用

23rd ACM/IEEE International Conference on Model Driven Engineering languages and Systems (MODELS)

作者： Cheng, Zheng Tisi, Massimo Hotonnier, Joachim Univ Lorraine LORIA CNRS INRIA Nancy France IMT Atlantique LS2N UMR 6004 CNRS Nantes France

ISBN: (纸本)9781450370196

Executable engines for relational model-transformation languages evolve continuously because of language extension, performance improvement and bug fixes. While new versions generally change the engine semantics, end-users expect to get backward-compatibility guarantees, so that existing transformations do not need to be adapted at every engine update. The CoqTL model-transformation language allows users to define model transformations, theorems on their behavior and machinechecked proofs of these theorems in Coq. Backward-compatibility for CoqTL involves also the preservation of these proofs. However, proof preservation is challenging, as proofs are easily broken even by small refactorings of the code they verify. In this paper we present the solution we designed for the evolution of CoqTL, and by extension, of rule-based transformation engines. We provide a deep specification of the transformation engine, including a set of theorems that must hold against the engine implementation. Then, at each milestone in the engine development, we certify the new version of the engine against this specification, by providing proofs of the impacted theorems. The certification formally guarantees end-users that all the proofs they write using the provided theorems will be preserved through engine updates. We illustrate the structure of the deep specification theorems, we produce a machine-checked certification of three versions of CoqTL against it, and we show examples of user theorems that leverage this specification and are thus preserved through the updates.

关键词： MDE Model Transformation programming language implementation Certification Theorem Proving Coq

来源：评论

学校读者我要写书评

暂无评论

Remote-Scope Promotion: Clarified, Rectified, and Verified 2015

Remote-Scope Promotion: Clarified, Rectified, and Verified

引用

ACM SIGPLAN International Conference on Object-Oriented programming, Systems, languages, and Applications (OOPSLA)

作者： Wickerson, John Batty, Mark Beckmann, Bradford M. Donaldson, Alastair F. Univ London Imperial Coll Sci Technol & Med London SW7 2AZ England Univ Kent Canterbury CT2 7NZ Kent England Adv Micro Devices Inc Sunnyvale CA 94088 USA

ISBN: (纸本)9781450336895

Modern accelerator programming frameworks, such as OpenCL (TM), organise threads into work-groups. Remote-scope promotion (RSP) is a language extension recently proposed by AMD researchers that is designed to enable applications, for the first time, both to optimise for the common case of intra-work-group communication (using memory scopes to provide consistency only within a work-group) and to allow occasional inter-work-group communication (as required, for instance, to support the popular load-balancing idiom of work stealing). We present the first formal, axiomatic memory model of OpenCL extended with RSP. We have extended the HERD memory model simulator with support for OpenCL kernels that exploit RSP, and used it to discover bugs in several litmus tests and a work-stealing queue, that have been used previously in the study of RSP. We have also formalised the proposed GPU implementation of RSP. The formalisation process allowed us to identify bugs in the description of RSP that could result in well-synchronised programs experiencing memory inconsistencies. We present and prove sound a new implementation of RSP that incorporates bug fixes and requires less non-standard hardware than the original implementation. This work, a collaboration between academia and industry, clearly demonstrates how, when designing hardware support for a new concurrent language feature, the early application of formal tools and techniques can help to prevent errors, such as those we have found, from making it into silicon.

关键词： Formal methods graphics processing unit (GPU) Isabelle OpenCL programming language implementation weak memory models work stealing

来源：评论

学校读者我要写书评

暂无评论

On Legality Assertions in Euclid

引用

IEEE Transactions on Software Engineering 1979年第4期SE-5卷 359-367页

作者： Wortman, David B. Department of Computer Science Computer Systems Research Group University of Toronto Toronto Ont. Canada Canada

The design of the programming language Euclid requires that a compiler for the language produce legality assertions to aid in verification of programs written in the language. This paper analyzes the legality assertions that must be produced and discusses the impact that this requirement has on the implementation of the language. Copyright © 1979 by The Institute of Electrical and Electronics Engineers, Inc.

关键词： Index Terms-Euclid legality assertions programming language design programming language implementation verification

来源：评论

学校读者我要写书评

暂无评论

Compiling mercury to high-level C code 11th

引用

11th International Conference on Compiler Construction (CC 2002)

作者： Henderson, F Somogyi, Z Univ Melbourne Dept Comp Sci & Software Engn Melbourne Vic 3010 Australia

ISBN: (纸本)3540433694

Many logic programming implementations compile to C, but they compile to very low-level C, and thus discard many of the advantages of compiling to a high-level language. We describe an alternative approach to compiling logic programs to C, based on continuation passing, that we have used in a new back-end for the Mercury compiler. The new approach compiles to much higher-level C code, which means the compiler back-end and run-time system can be considerably simpler. We present a formal schema for the transformation, and give benchmark results which show that this approach delivers performance that is more than competitive with the fastest previous implementation, with greater simplicity and better portability and interoperability. The approach we describe can also be used for compiling to other target languages, such as IL (the Microsoft NET intermediate language).

关键词： compilation techniques programming language implementation logic programming Mercury C GNU C

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：