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

COMPUTER 1996年第3期29卷 109-111页

作者： McKim, JC Dept. of Comput. & Inf. Sci. Hartford Graduate Center CT USA

Why can't software be more like hardware? has been the software engineer'slament for nearly as long as there have been large software systems. In particular, why isn't therea software components industry to rival the existing hardware components industry? Hardwarecomponents come with the following attributes: an interface that hides detail that would onlyconfuse or at least distract me; an unambiguous interface specification written in a language I canunderstand (in the case of the integrated circuit, this may be a fairly complex language, but it'sone I expect to learn if I'm going to work with that hardware); a guarantee-the component has beentested and/or validated against its specification. All three items-especially the last one-arenotably lacking for software components. Indeed, software tends to come with an antiguarantee,otherwise known as a disclaimer. All of the above points rely on a rigorous specification of thehardware component's interface. In a nutshell, programming by contract is about providing just suchspecifications for software components (that is, classes), and it provides the best hope of a basisfor a true software component industry. The discussion focuses on object oriented software.

关键词： Economics Object Oriented programming contracts Formal Specification User Interfaces DP Industry Object Oriented Software programming by contract Large Software Systems Software Components Industry Hardware Components Industry Interface Unambiguous Interface Specification Guarantee Software Components Disclaimer Rigorous Specification Classes contracts Computer Industry Application Software

来源：评论

学校读者我要写书评

暂无评论

A framework for the static verification of API calls

引用

JOURNAL OF SYSTEMS AND SOFTWARE 2007年第7期80卷 1156-1168页

作者： Spinellis, Diomidis Louridas, Panagiotis Athens Univ Economist & Business Dept Management Sci & Technol GR-10434 Athens Greece

A number of tools can statically check program code to identify commonly encountered bug patterns. At the same time, programs are increasingly relying on external APIS for performing the bulk of their work: the bug-prone program logic is being fleshed-out, and many errors involve tricky subroutine calls to the constantly growing set of external libraries. Extending the static analysis tools to cover the available APIS is an approach that replicates scarce human effort across different tools and does not scale. Instead, we propose moving the static API call verification code into the API implementation, and distributing the verification code together with the library proper. We have designed a framework for providing static verification code together with Java classes, and have extended the FindBugs static analysis tool to check the corresponding method invocations. To validate our approach we wrote verification tests for 100 different methods, and ran FindBugs on 6.9 million method invocations on what amounts to about 13 million lines of production-quality code. In the set of 55 thousand method invocations that could potentially be statically verified our approach identified 800 probable errors. (C) 2006 Elsevier Inc. All rights reserved.

关键词： static analysis API library programming by contract FindBugs

来源：评论

学校读者我要写书评

暂无评论

Engineering a Sound Assertion Semantics for the Verifying Compiler

引用

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING 2010年第2期36卷 275-287页

作者： Chalin, Patrice Concordia Univ Dependable Software Res Grp Comp Sci & Software Engn Dept Montreal PQ Canada

The Verifying Compiler ( VC) project is a core component of the Dependable Systems Evolution Grand Challenge. The VC offers the promise of automatically proving that a program or component is correct, where correctness is defined by program assertions. While several VC prototypes exist, all adopt a semantics for assertions that is unsound. This paper presents a consolidation of VC requirements analysis ( RA) activities that, in particular, brought us to ask targeted VC customers what kind of semantics they wanted. Taking into account both practitioners' needs and current technological factors, we offer recovery of soundness through an adjusted definition of assertion validity that matches user expectations and can be implemented practically using current prover technology. For decades, there have been debates concerning the most appropriate semantics for program assertions. Our contribution here is unique in that we have applied fundamental software engineering techniques by asking primary stakeholders what they want and, based on this, proposed a means of efficiently realizing the semantics stakeholders want using standard tools and techniques. We describe how support for the new semantics has been added to ESC/Java2, one of the most fully developed VC prototypes. Case studies demonstrate the effectiveness of the new semantics at uncovering previously indiscernible specification errors.

关键词： Software verification assertions programming by contract logics of programs requirements engineering

来源：评论

学校读者我要写书评

暂无评论

Design by contract to improve software vigilance

引用

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING 2006年第8期32卷 571-586页

作者： Le Traon, Yves Baudry, Benoit Jezequel, Jean-Marc France Telecom R&D F-22307 Lannion France Univ Rennes 1 IRISA F-35042 Rennes France

Design by contract is a lightweight technique for embedding elements of formal specification ( such as invariants, pre and postconditions) into an object-oriented design. When contracts are made executable, they can play the role of embedded, online oracles. Executable contracts allow components to be responsive to erroneous states and, thus, may help in detecting and locating faults. In this paper, we define Vigilance as the degree to which a program is able to detect an erroneous state at runtime. Diagnosability represents the effort needed to locate a fault once it has been detected. In order to estimate the benefit of using Design by contract, we formalize both notions of Vigilance and Diagnosability as software quality measures. The main steps of measure elaboration are given, from informal definitions of the factors to be measured to the mathematical model of the measures. As is the standard in this domain, the parameters are then fixed through actual measures, based on a mutation analysis in our case. Several measures are presented that reveal and estimate the contribution of contracts to the overall quality of a system in terms of vigilance and diagnosability.

关键词： object-oriented design methods programming by contract diagnostics metrics

来源：评论

学校读者我要写书评

暂无评论

A framework for conceptual modeling in OOP

引用

JOURNAL OF THE FRANKLIN INSTITUTE-ENGINEERING AND APPLIED MATHEMATICS 2006年第4-5期343卷 532-544页

作者： Al-Ahmad, Walid New York Inst Technol Sch Engn & Technol Manama Bahrain

There are several language constructs and mechanisms that provide some sort of support for conceptual modeling in object-oriented programming: the Liskov substitution principle, the Meyer programming by contract, the Beta inner construct, interfaces in C# and Java, and the separation of subtype hierarchies from subclass hierarchies as in Timor and Sather. All these mechanisms and constructs are powerful and useful tools to enforce the conceptual modeling trait of the inheritance mechanism in object-oriented programming. Their purpose is to ensure semantic compatibility of classes related by an inheritance hierarchy. When applied independently, these mechanisms can lead to more correct inheritance hierarchies that are easy to understand, use, and extend. This article discusses the different mechanisms and studies the interaction between them. It investigates whether conceptual modeling can be satisfactorily achieved by using such tools. It will be shown that the interaction between these tools might lead to contradictions and might prevent legitimate inheritance hierarchies. This article proposes a framework for a conceptual modeling mechanism that will better support conceptual modeling at the language level. (C) 2006 The Franklin Institute. Published by Elsevier Ltd. All rights reserved.

关键词： programming by contract Liskov substitution principle inheritance conceptual modeling

来源：评论

学校读者我要写书评

暂无评论

How the design of JML accommodates both runtime assertion checking and formal verification

引用

SCIENCE OF COMPUTER programming 2005年第1-3期55卷 185-208页

作者： Leavens, GT Cheon, Y Clifton, C Ruby, C Cok, DR Iowa State Univ Dept Comp Sci Ames IA USA Univ Texas Dept Comp Sci El Paso TX 79968 USA Eastman Kodak Co Res & Dev Labs Rochester NY USA

Specifications that are used in detailed design and in the documentation of existing code are primarily written and read by programmers. However, most formal specification languages either make heavy use of symbolic mathematical operators, which discourages use by programmers, or limit assertions to expressions of the underlying programming language, which makes it difficult to write exact specifications. Moreover, using assertions that are expressions in the underlying programming language can cause problems both in runtime assertion checking and in formal verification, because such expressions can potentially contain side effects. The Java Modeling Language, JML, avoids these problems. It uses a side-effect free subset of Java's expressions to which are added a few mathematical operators (such as the quantifiers \forall and \exists). JML also hides mathematical abstractions, such as sets and sequences, within a library of Java classes. The goal is to allow JML to serve as a common notation for both formal verification and runtime assertion checking;this gives users the benefit of several tools without the cost of changing notations. (C) 2004 Elsevier B.V. All rights reserved.

关键词： specification languages runtime assertion checking formal methods program verification programming by contract Java language JML language

来源：评论

学校读者我要写书评

暂无评论

Specifying and checking method call sequences of Java programs

引用

SOFTWARE QUALITY JOURNAL 2007年第1期15卷 7-25页

作者： Cheon, Yoonsik Perumandla, Ashaveena Univ Texas Dept Comp Sci El Paso TX 79968 USA

In a pre and postcondition-style specification, it is difficult to specify the allowed sequences of method calls, referred to as protocols. The protocols are essential properties of reusable object-oriented classes and application frameworks, and the approaches based on the pre and postconditions, such as design by contracts (DBC) and formal behavioral interface specification languages (BISL), are being accepted as a practical and effective tool for describing precise interfaces of (reusable) program modules. We propose a simple extension to the Java Modeling Language (JML), a BISL for Java, to specify protocol properties in an intuitive and concise manner. The key idea of our approach is to separate protocol properties from functional properties written in pre and post-conditions and to specify them in a regular expression-like notation. The semantics of our extension is formally defined and provides a foundation for implementing runtime checks. Case studies have been performed to show the effectiveness our approach. We believe that our approach can be adopted by other BISLs.

关键词： method call sequence specification runtime checking assertion pre and postconditions programming by contract JML language

来源：评论

学校读者我要写书评

暂无评论

Special Session: "Hands-On" Tutorial: Teaching Software Correctness with RESOLVE 14

Special Session: "Hands-On" Tutorial: Teaching Software Corr...

引用

45th ACM SIGCSE Technical Symposium on Computer Science Education (SIGCSE)

作者： Sitaraman, Murali Weide, Bruce W. Clemson Univ Sch Comp Clemson SC 29634 USA Ohio State Univ Comp Sci & Engn Columbus OH 43210 USA

ISBN: (纸本)9781450326056

Program correctness is central to computing, with instructors striving to convey the importance of "getting it right" starting in CS1. Teaching this material carefully demands a uniform framework to specify, implement, and reason about software correctness. To make these ideas accessible to educators and students, the tutorial will use RESOLVE, an integrated specification and programming language with a toolset especially designed for building verified components. The tutorial will also discuss how to get students involved through hands-on activities with software construction and modular verification using a web-integrated environment that requires no software installation and that features a prototype "push-button" verifying compiler. The proposers have taught the ideas contained here using engaging pedagogical methods in introductory and advanced CS courses to thousands of students and dozens of educators over the past 20 years, and this SIGCSE tutorial will leverage that experience.

关键词： Components correctness proofs programming by contract specification verification

来源：评论

学校读者我要写书评

暂无评论

Design by contract Framework for Quantum Software 4

Design by Contract Framework for Quantum Software

引用

4th IEEE/ACM International Workshop on Quantum Software Engineering (Q-SE)

作者： Yamaguchi, Masaomi Yoshioka, Nobukazu Fujitsu Ltd Quantum Lab Kanagawa Japan Waseda Univ Natl Inst Informat Tokyo Japan

ISBN: (纸本)9798350301809

To realize reliable quantum software, techniques to automatically ensure the quantum software's correctness have recently been investigated. However, they primarily focus on fixed quantum circuits rather than the procedure of building quantum circuits. Despite being a common approach, the correctness of building circuits using different parameters following the same procedure is not guaranteed. To this end, we propose a designby-contract framework for quantum software. Our framework provides a python-embedded language to write assertions on the input and output states of all quantum circuits built by certain procedures. Additionally, it provides a method to write assertions about the statistical processing of measurement results to ensure the procedure's correctness for obtaining the final result. These assertions are automatically checked using a quantum computer simulator. For evaluation, we implemented our framework and wrote assertions for some widely used quantum algorithms. Consequently, we found that our framework has sufficient expressive power to verify the whole procedure of quantum software.

关键词： programming by contract Testing and Debugging quantum computing

来源：评论

学校读者我要写书评

暂无评论

Special Session: Engaging Mathematical Reasoning Exercises 14

Special Session: Engaging Mathematical Reasoning Exercises

引用

45th ACM SIGCSE Technical Symposium on Computer Science Education (SIGCSE)

作者： Hollingsworth, Joseph Sitaraman, Murali Indiana Univ Southeast Comp Sci New Albany IN 47150 USA Clemson Univ Sch Comp Clemson SC 29634 USA

ISBN: (纸本)9781450326056

At SIGCSE 2013 this special session [1] provided attendees interested in math thinking a place where engaging math reasoning examples and assignments that help connect mathematics and software development could be shared and discussed. The exercises and assignments presented last year were well received by the audience who indicated immediately that they would find ways to incorporate them in classes such as CS1, CS2, data structures and algorithms, discrete math, and software engineering courses. Feedback from our own surveys showed that even as there was much interest in using engaging math reasoning examples, there was also considerable interest in developing new engaging math reasoning assignments for future sessions. Based on these expressions of interest and the general interest of the approximately 100 attendees of last year's special session, we feel compelled to continue the momentum by proposing a second round of this forum for SIGCSE 2014. We have contact information for these potential presenters and we expect to have no difficulty in attracting suitable presenters if the session is accepted. The remainder of this proposal is nearly identical to last year's proposal except for the example that appears in Section 2. That example is drawn directly from one of the engaging reasoning assignments presented at last year's special session. All exercises are available at [2].

关键词： Correctness proofs discrete structures induction invariants programming by contract specification verification

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：