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

16th Asia-Pacific Software Engineering Conference

作者： Wang, Chen-Wei Cavarra, Alessandra Univ Oxford Comp Lab Oxford OX1 3QD England

ISBN: (纸本)9780769539096

In model-driven development, requirements are captured as a specification model, from which a conforming implementation is automatically generated. Model consistency, with respect to requirements, is a primary concern. If the various structural and integrity constraints are inconsistent, then either the model will admit no implementation, or the implementation produced will not behave according to the intended requirements. We present an approach, based upon data-How testing, to helping developers inspect their models for inconsistency. System models contain classes, attributes, invariants, and methods specified as first-order predicates. We identify for every attribute its intra-method usages. We construct accordingly call sequences demonstrating its inter-method usages. We derive from each call sequence a Boolean constraint, as a test case, ensuring both the execution of the corresponding inter-method usage and the maintenance of invariants. Developers may examine this test suite and compare against their original understandings about the requirements.

关键词： object-oriented design methods model consistency data-flow analysis formal methods programming by contract

来源：评论

学校读者我要写书评

暂无评论

Specifying and checking method call sequences of Java programs

Specifying and checking method call sequences of Java progra...

引用

International Conference on Software Engineering Research and Practice (SERP'05)

作者： 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

来源：评论

学校读者我要写书评

暂无评论

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

How the design of JML accommodates both runtime assertion ch...

引用

1st International Symposium on Formal Methods for Components and Objects

作者： Leavens, GT Cheon, Y Clifton, C Ruby, C Cok, DR Iowa State Univ Sci & Technol Dept Comp Sci Ames IA 50011 USA Eastman Kodak Co Res & Dev Labs Rochester NY 14650 USA

ISBN: (纸本)3540203036

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 complete 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.

关键词： Formal methods Java language JML language Program verification programming by contract Runtime assertion checking Specification languages

来源：评论

学校读者我要写书评

暂无评论

A Practical Approach to Assertion Testing Framework based on Inner Class

A Practical Approach to Assertion Testing Framework based on...

引用

2011 2nd IEEE International Conference on Software Engineering and Service Science(2011年第二届 IEEE 软件工程与服务科学国际会议 ICSESS 2011)

作者： Guodong Qu Hongqun Zhang Song-Tao Guo Center for Earth Observation and Digital Earth Chinese Academy of Sciences Beijing 100086 China Department of Mathematics Beijing Jiaotong University Beijing 100044 China

Using logical assertions for program verification is a basic research subject in software engineering. This paper analyzes current approaches and proposes three rules that an assertion testing framework should satisfy. That is, after adding contracts using a framework, the contracts in a tested project should be able to satisfy consistency, transitivity and completeness. By satisfying these three rules, the contracts can perform as a solid foundation for automatic test case generation. This paper also brings forward a practical approach to writing contracts, the Java Test Oracle Creator (jtoc), which uses Java annotations and Java inner class to construct intelligible contracts for programmers. Finally, a proof is given that jtoc-generated test projects satisfy the three rules proposed above.

关键词： assertion checkers programming by contract program verification software testing

来源：评论

学校读者我要写书评

暂无评论

A Practical Approach to Assertion Testing Framework based on Inner Class

A Practical Approach to Assertion Testing Framework based on...

引用

2011 IEEE 2nd International Conference on Software Engineering and Service Science(ICSESS 2011)

作者： Guodong Qu Center for Earth Observation and Digital Earth Chinese Academy of Sciences Beijing, 100086, China Song-Tao Guo Department of Mathematics Beijing Jiaotong University Beijing, 100044, China Hongqun Zhang Center for Earth Observation and Digital Earth Chinese Academy of Sciences Beijing, 100086, China

Using logical assertions for program verification is a basic research subject in software engineering. This paper analyzes current approaches and proposes three rules that an assertion testing framework should satisfy. That is, after adding contracts using a framework, the contracts in a tested project should be able to satisfy consistency, transitivity and completeness. By satisfy- ing these three rules, the contracts can perform as a solid foundation for automatic test case generation. This pa- per also brings forward a practical approach to writing contracts, the Java Test Oracle Creator (jtoc), which uses Java annotations and Java inner class to construct intelligible contracts for programmers. Finally, a proof is given that jtoc-generated test projects satisfy the three rules proposed above.

关键词： assertion checkers programming by contract pro- gram verification software testing

来源：评论

学校读者我要写书评

暂无评论

contract-based data structure repair using alloy 10

Contract-based data structure repair using alloy

引用

Proceedings of the 24th European conference on Object-oriented programming

作者： Razieh Nokhbeh Zaeem Sarfraz Khurshid University of Texas Austin TX

ISBN: (纸本)9783642141065

contracts and specifications have long been used in object-oriented design, programming and testing to enhance reliability before software deployment. However, the use of specifications in deployed software is commonly limited to runtime checking where assertions form a basis for detecting incorrect program states to terminate the erroneous executions. This paper presents a contract-based approach for data structure repair, which allows repairing erroneous executions in deployed software by repairing erroneous states. The key novelty is the support for rich behavioral specifications, such as those that relate pre-states with post-states of the method to accurately specify expected behavior and hence to enable precise repair. The approach is based on the view of a specification as a nondeterministic implementation, which may permit a high degree of non-determinism. The key insight is to use any correct state mutations by an otherwise erroneous execution to prune the non-determinism in the specification, thereby transmuting the specification to an implementation that does not incur a prohibitively high performance penalty. While invariants, pre-conditions and post-conditions could be provided in different modeling languages, we leverage the Alloy tool-set, specifically the Alloy language and the Alloy Analyzer for systematically repairing erroneous states. Four different algorithms are presented and implemented in our data structure repair framework. Experiments using complex specifications show the approach holds much promise in increasing software reliability.

关键词： specifications Alloy programming by contract data structure repair

来源：评论

学校读者我要写书评

暂无评论

Engaging mathematical reasoning exercises 13

Engaging mathematical reasoning exercises

引用

Proceeding of the 44th ACM technical symposium on Computer science education

作者： Joseph Hollingsworth Joan Krone Jason Hallstrom Murali Sitaraman Bruce Weide Indiana University Southeast New Albany IN USA Denison University Granville OH USA Clemson University Clemson SC USA The Ohio State University Columbus OH USA

No abstract available.

ISBN: (纸本)9781450318686

No abstract available.

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

来源：评论

学校读者我要写书评

暂无评论

Black-box testing using flowgraphs: an experimental assessment of effectiveness and automation potential

引用

Software Testing, Verification and Reliability 2001年第4期10卷

作者： Stephen H. Edwards Department of Computer Science Virginia Tech 660 McBryde Hall Blacksburg VA 24061–0106 U.S.A.

A black-box testing strategy based on Zweben et al.'s specification-based test data adequacy criteria is explored. The approach focuses on generating a flowgraph from a component's specification and applying analogues of white-box strategies to it. An experimental assessment of the fault-detecting ability of test sets generated using this approach was performed for three of Zweben et al.'s criteria using mutation analysis. By using precondition, postcondition and invariant checking wrappers around the component under test, fault detection ratios competitive with white-box techniques were achieved. Experience with a prototype test set generator used in the experiment suggests that practical automation may be feasible. Copyright © 2000 John Wiley & Sons, Ltd.

关键词： automatic testing object-oriented testing test data adequacy formal specification programming by contract interface violation detection self-checking software

来源：评论

学校读者我要写书评

暂无评论

Constructing contracts: Making discrete mathematics relevant to beginning programmers

引用

Journal on Educational Resources in Computing 2005年第2期5卷 3–es页

作者： Timothy S. Gegg-Harrison Winona State University Winona MN

Although computer scientists understand the importance of discrete mathematics to the foundations of their field, computer science (CS) students do not always see the relevance. Thus, it is important to find a way to show students its relevance. The concept of program correctness is generally taught as an activity independent of the programming process, hence many CS students perceive it as unnecessary, and even irrelevant. The concept of contracts, on the other hand, is generally taught as an integral part of the programming process. Most CS students have little difficulty understanding the need to establish contracts via preconditions and postconditions. In order to improve teaching program correctness concepts, we implemented ProVIDE, an enhanced integrated development environment (IDE). ProVIDE assists student programmers in contract construction. Rather than asking for both a precondition and postcondition for each of the student's methods, ProVIDE asks the student to simply supply a postcondition. ProVIDE then helps the student construct the appropriate precondition by leading him or her through an axiomatic proof of the method's correctness. Thus, the proof of of the method's correctness is a side-effect of the student's need to construct an appropriate precondition.

关键词： Formal methods axiomatic semantics loop invariants program verification programming by contract programming tools weakest preconditions

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：