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

INFERENCE RULES FOR program annotation

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING 1981年第2期7卷 207-222页

作者： DERSHOWITZ, N MANNA, Z STANFORD UNIV DEPT COMP SCISTANFORDCA 94305 WEIZMANN INST SCI DEPT APPL MATHREHOVOT 76100ISRAEL

Methods are presented whereby documentation can be accomplished automatically for an Algol-like program given together with its specifications. The program is incrementally annotated with invariant relations that hold between program variables at intermediate points in the program text and explain the actual workings of the program, regardless of whether or not it is correct. Thus, it follows that such documentation can be utilized for proving correctness of programs, and it may also serve as an aid in debugging incorrect programs. The annotation techniques are formulated as Hoare-like inference rules that derive invariants from: 1. assignment statements, 2. control structure of the program, or 3. suggested invariants (heuristically). Examples that have run on an experimental implementation serve to demonstrate the application of these rules.

关键词： Verification Inference Rules Invariant Assertions program annotation program Correctness

来源：评论

学校读者我要写书评

暂无评论

Inference rules for program annotation 78

Inference rules for program annotation

引用

Proceedings of the 3rd international conference on Software engineering

作者： Nachum Dershowitz Zohar Manna

Methods are presented whereby an Algol-like program, given together with its specifications, can be documented automatically. The program is incrementally annotated with invariant relationships that hold between program variables at intermediate points in the program and explain the actual workings of the program regardless of whether the program is correct. Thus this documentation can be used for proving the correctness of the program or may serve as an aid in the debugging of an incorrect *** annotation techniques are formulated as Hoare-like inference rules which derive invariants from the assignment statements, from the control structure of the program, or, heuristically, from suggested invariants. The application of these rules is demonstrated by an example, one of a number that have run on an experimental implementation.

关键词： Verification program annotation program correctness Invariant assertions Inference rules

来源：评论

学校读者我要写书评

暂无评论

Data Flow Analysis as a General Concept for the Transport of Verifiable program annotations

引用

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2007年第3期176卷 97-108页

作者： Amme, Wolfram Moeller, Marc-Andre Adler, Philipp Friedrich Schiller Univ Jena Inst Informat Jena Germany

Just-in-Time (JIT) compilation is frequently employed in order to speed-up the execution of platfor-independent and dynamically extensible mobile code applications. Since the time required for dynamic compilation directly influences a program's execution time, JIT compilers usually utilize only simple and fast techniques for program analysis and optimization. To improve further the analysis and optimization process of such compilers program annotations can be used. However, mostly all current annotation approaches suffer from the fact that the verification of transmitted program information is time consuming and therefore will not be carried out on the consumer side of a mobile code system. In this paper, we present a verifiable annotation technique that is based on a well known iterative data flow algorithm and which can be used for the transmission of all program information that can be derived through data flow analysis. Preliminary measurements of compilation and verification time indicate that the presented technique seems to be implementable and therefore could be used as an all-purpose transportation technique for safe program annotations.

关键词： Data Flow Analysis program annotation Verifikation

来源：评论

学校读者我要写书评

暂无评论

Guided just-in-time specialization

引用

SCIENCE OF COMPUTER programMING 2020年 185卷 102318-102318页

作者： Lima, Caio Cezar, Junio Leobas, Guilherme Vieira Rohou, Erven Quintao Pereira, Fernando Magno Ave Antonio Carlos 6627 Belo Horizonte MG Brazil Univ Rennes Inria CNRS IRISA Rennes France

JavaScript's portability across a vast ecosystem of browsers makes it today a core building block of the web. Yet, building efficient systems in JavaScript is still challenging. Because this language is so dynamic, JavaScript programs provide little information that just-in-time compilers can use to carry out safe optimizations. Motivated by this observation, we propose to guide the JIT compiler in the task of code specialization. To this end, we have augmented the language with an annotation that indicates which function call sites are likely to benefit from specialization. To support the automatic annotation of programs, we have introduced a novel static analysis that identifies profitable specialization points. We have implemented our ideas in JavaScriptCore, the built-in JavaScript engine for WebKit. The addition of guided specialization to this engine required us to change it in several non-trivial ways, which we describe in this paper. Such changes let us observe speedups of up to 1.7x on programs present in synthetic benchmarks. (C) 2019 Elsevier B.V. All rights reserved.

关键词： Code specialization Just-in-time compilation program annotation Performance JavaScript

来源：评论

学校读者我要写书评

暂无评论

CLPGUI: A generic graphical user interface for constraint logic programming

引用

CONSTRAINTS 2004年第4期9卷 241-262页

作者： Fages, F Soliman, S Coolen, R INRIA Rocquencourt Projet Contraintes F-78153 Le Chesnay France

CLPGUI is a generic graphical user interface for visualizing and controlling the execution of constraint logic programs. CLPGUI has been designed to be used in different contexts: initially for teaching purposes, then for debugging complex programs of real-world scale, and recently for developing end-user interfaces. The challenge of developing a tool which is generic w.r.t. both the constraint logic programming system and the visualizers, is addressed by a client-server architecture for connecting a CLP process to a Java-based GUI process, and by a non-intrusive tracing and control method based on annotations in the CLP program. Arbitrary constraints and goals can be posted incrementally from the GUI in an interactive manner, and arbitrary states can be recomputed. We describe several generic 2D and 3D viewers of the variables and of the search tree, and argue that the 3D representation is best-suited to apprehend the shape of large search trees. We also illustrate the use of CLPGUI for developing application-oriented end-user interfaces on two placement problems, one in virtual reality.

关键词： constraint programming visualization program annotation GUI search trees debugging

来源：评论

学校读者我要写书评

暂无评论

A Survey of Automatic Generation of Source Code Comments: Algorithms and Techniques

引用

IEEE ACCESS 2019年 7卷 111411-111428页

作者： Song, Xiaotao Sun, Hailong Wang, Xu Yan, Jiafei Taiyuan Univ Technol Sch Software Taiyuan 030024 Shanxi Peoples R China Beihang Univ Sch Comp Sci & Engn SKLSDE Lab Beijing 100191 Peoples R China Beihang Univ Beijing Adv Innovat Ctr Big Data & Brain Comp Beijing 100191 Peoples R China Beijing Aeronaut Sci & Technol Res Inst Beijing 102211 Peoples R China Beijing Key Lab Civil Aircraft Design & Simulat T Beijing 102211 Peoples R China

As an integral part of source code files, code comments help improve program readability and comprehension. However, developers sometimes do not comment their program code adequately due to the incurred extra efforts, lack of relevant knowledge, unawareness of the importance of code commenting or some other factors. As a result, code comments can be inadequate, absent or even mismatched with source code, which affects the understanding, reusing and the maintenance of software. To solve these problems of code comments, researchers have been concerned with generating code comments automatically. In this work, we aim at conducting a survey of automatic code commenting researches. First, we generally analyze the challenges and research framework of automatic generation of program comments. Second, we present the classification of representative algorithms, the design principles, strengths and weaknesses of each category of algorithms. Meanwhile, we also provide an overview of the quality assessment of the generated comments. Finally, we summarize some future directions for advancing the techniques of automatic generation of code comments and the quality assessment of comments.

关键词： Code comment deep learning information retrieval machine learning program annotation

来源：评论

学校读者我要写书评

暂无评论

Page Placement Strategies for GPUs within Heterogeneous Memory Systems 15

Page Placement Strategies for GPUs within Heterogeneous Memo...

引用

20th International Conference on Architectural Support for programming Languages and Operating Systems (ASPLOS)

作者： Agarwal, Neha Nellans, David Stephenson, Mark O'Connor, Mike Keckler, Stephen W. Univ Michigan Ann Arbor MI 48109 USA NVIDIA Westford MA USA

ISBN: (纸本)9781450328357

Systems from smartphones to supercomputers are increasingly heterogeneous, being composed of both CPUs and GPUs. To maximize cost and energy efficiency, these systems will increasingly use globally-addressable heterogeneous memory systems, making choices about memory page placement critical to performance. In this work we show that current page placement policies are not sufficient to maximize GPU performance in these heterogeneous memory systems. We propose two new page placement policies that improve GPU performance: one application agnostic and one using application profile information. Our application agnostic policy, bandwidth-aware (BW-AWARE) placement, maximizes GPU throughput by balancing page placement across the memories based on the aggregate memory bandwidth available in a system. Our simulation-based results show that BW-AWARE placement outperforms the existing Linux INTERLEAVE and LOCAL policies by 35% and 18% on average for GPU compute workloads. We build upon BW-AWARE placement by developing a compiler-based profiling mechanism that provides programmers with information about GPU application data structure access patterns. Combining this information with simple program-annotated hints about memory placement, our hint-based page placement approach performs within 90% of oracular page placement on average, largely mitigating the need for costly dynamic page tracking and migration.

关键词： Bandwidth Page placement Linux program annotation

来源：评论

学校读者我要写书评

暂无评论

Bootstrapping Privacy Compliance in Big Data Systems 35

Bootstrapping Privacy Compliance in Big Data Systems

引用

35th IEEE-Computer-Society Workshop on Security and Privacy (SP)

作者： Sen, Shayak Guha, Saikat Datta, Anupam Rajamani, Sriram K. Tsai, Janice Wing, Jeannette M. Carnegie Mellon Univ Pittsburgh PA 15213 USA Microsoft Res Bangalore Karnataka India Microsoft Res Redmond WA USA

ISBN: (纸本)9781479946860

With the rapid increase in cloud services collecting and using user data to offer personalized experiences, ensuring that these services comply with their privacy policies has become a business imperative for building user trust. However, most compliance efforts in industry today rely on manual review processes and audits designed to safeguard user data, and therefore are resource intensive and lack coverage. In this paper, we present our experience building and operating a system to automate privacy policy compliance checking in Bing. Central to the design of the system are (a) LEGALEASE-a language that allows specification of privacy policies that impose restrictions on how user data is handled;and (b) GROK-a data inventory for Map-Reduce-like big data systems that tracks how user data flows among programs. GROK maps code-level schema elements to datatypes in LEGALEASE, in essence, annotating existing programs with information flow types with minimal human input. Compliance checking is thus reduced to information flow analysis of big data systems. The system, bootstrapped by a small team, checks compliance daily of millions of lines of ever-changing source code written by several thousand developers.

关键词： Big Data Web services cloud computing computer bootstrapping conformance testing data privacy parallel programming search engines source code (software) Bing Grok data inventory Legal ease language Map-Reduce-like Big Data systems automatic privacy policy compliance checking business imperative privacy policies cloud services code-level schema element mapping datatypes information flow types minimal human input personalized user experiences privacy compliance bootstrapping privacy policy specification program annotation source code user data handling user trust Advertising Big data Data privacy IP networks Lattices Privacy Semantics big data bing compliance information flow policy privacy program analysis big data spoil heaps Data privacy Privacy Cloud Computing user data information flow Source code conformance testing data types analysis programme Internet Protocol networks Parallel programming Advertising as Topic Search engines

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：