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

A survey on formal, object-oriented program development approaches

SCIENTIA IRANICA 2015年第3期22卷 1001-1017页

作者： Najafi, M. Haghighi, H. Nasab, T. Zohdi Shahid Beheshti Univ Fac Elect & Comp Engn Tehran Iran

Due to the popularity of object-oriented programming approaches, there is a growing interest in utilizing object-oriented concepts, such as encapsulation and reuse, when applying formal methods. The main contribution of this paper is to review and compare existing formal methods to develop object-oriented programs from formal specifications. The secondary contribution is providing a comparison between widely used object-oriented formal specification languages. The results of this paper can be utilized by researchers wishing to know what open problems are outstanding in the areas of formal, object-oriented specification and program development. Our findings are also useful for those who are looking for proper specification languages and program development methods to specify and develop object-oriented programs formally. In addition, the provided criteria are suitable for evaluating numerous object-oriented formal specification languages that are under development, either by extending existing formal approaches or formalizing informal OO-methods. As one consequence of this work, it can be mentioned that among formal specification languages, OZ and VDM++ support 00 concepts more strongly in comparison to VDM++ and UML-B. program development methods based on OZ have less tool support. Finally, most proposed methods for formal, object-oriented program development have been evaluated using only case studies, rather than employing formal approaches. (C) 2015 Sharif University of Technology. All rights reserved.

关键词： formal program development Object-orientation formal specification Object-Z VDM VDM plus B Event-B UML-B

来源：评论

学校读者我要写书评

暂无评论

Essential Concepts of Algebraic Specification and program development

引用

formal Aspects of Computing 1997年第3期9卷 229-269页

作者： Sannella, Donald Tarlecki, Andrzej LFCS Department of Computer Science University of Edinburgh Edinburgh United Kingdom Institute of Informatics Warsaw University Institute of Computer Science Warsaw Poland LFCS Department of Computer Science University of Edinburgh Edinburgh EH9 3JZ United Kingdom

The main ideas underlying work on the model-theoretic foundations of algebraic specification and formal program development are presented in an informal way. An attempt is made to offer an overall view, rather than ne... 详细信息

关键词： Algebraic specification Behavioural equivalence formal program development Implementation of specifications Specification and program structure

来源：评论

学校读者我要写书评

暂无评论

An approach to animate Object-Z specifications using C plus

引用

SCIENTIA IRANICA 2012年第6期19卷 1699-1721页

作者： Najafi, M. Haghighi, H. Shahid Beheshti Univ Fac Elect & Comp Engn Tehran Iran

Object-Z is an extension of the Z notation which facilitates specification of large, complex software by defining a system as a collection of independent classes. A number of contributions have been made so far to map Object-Z to various object-oriented languages. However, the given mapping approaches do not cover several Object-Z specification constructs, such as class union, object aggregation, object containment and some of the operation operators. Also, in much of the existing work, mapping rules are given in a very abstract form. In other words, they do not consider all cases in a detailed way needed to automate the mapping procedure. In our previous work, we partially tackled these issues;however, in this paper, we present a much more comprehensive way to animate Object-Z specifications using C++. The given method covers some constructs that have not been addressed in our previous work. Also, mapping rules are described with enough details facilitating automation. Finally, we consider some level of user interaction in our new method which increases the flexibility and efficiency of final codes from the user point of view. (C) 2012 Sharif University of Technology. Production and hosting by Elsevier B.V. All rights reserved.

关键词： formal program development Object-oriented programming Animation Object-Z C plus

来源：评论

学校读者我要写书评

暂无评论

Nondeterminism in Constructive Z

引用

FUNDAMENTA INFORMATICAE 2008年第1-2期88卷 109-134页

作者： Haghighi, Hassan Mirian-Hosseinabadi, Seyed-Hassan Sharif Univ Technol Dept Comp Engn Tehran Iran

The abstraction inherent in most specifications and the need to specify nondeterministic programs are two well-known sources of nondeterminism in formal specifications. In this paper, we present a Z-based formalism by which one can specify bounded, unbounded, erratic, angelic, demonic, loose, strict, singular, and plural nondeterminism. To interpret our specifications, we use a constructive set theory, called CZ set theory, instead of the classical set theory Z. We have chosen CZ since it allows us to investigate the notion of nondeterminism from the formal program development point of view. In this way, we formally construct functional programs from Z specifications and then probe the effects of the initially specified nondeterminism on final programs. Our investigation shows that without specifying nondeterminism explicitly, the effects of the nondeterminism involved in initial specifications will not be preserved in final programs. We prove that using the new formalism, proposed by this paper, for writing nondeterministic specifications leads to programs that preserve the initially specified modalities of nondeterminism.

关键词： formal specification formal program development constructive Z Martin-Lof's theory of types nondeterminism modalities of nondeterminism

来源：评论

学校读者我要写书评

暂无评论

A linear approximation algorithm for bin packing with absolute approximation factor 3/2

引用

SCIENCE OF COMPUTER programMING 2003年第1期48卷 67-80页

作者： Berghammer, R Reuter, F Univ Kiel Inst Informat & Prakt Math D-24098 Kiel Germany

We present a new approximation algorithm for the bin packing problem which has a linear running time and an absolute approximation factor of 3/2. It is known that this approximation factor is the best factor achievabl... 详细信息

关键词： bin packing approximation algorithm formal program development

来源：评论

学校读者我要写书评

暂无评论

An Approach to Nondeterminism in Translation of CZ Set Theory into Martin-Lof 's Theory of Types

引用

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2006年第1期159卷 117-137页

作者： Haghighi, Hassan Hosseinabadi, Seyyed Hassan Mirian Sharif Univ Technol Dept Comp Engn Tehran Iran

Due to the high level of abstraction involved in formal specification of software systems, nondeterminism comes as an inevitable part of formal specifications. Therefore, support for nondeterminism should be provisioned in developing programs from their formal specifications. In this paper, an existing translation of CZ set theory into Martin- Lof's theory of types is extended to consider nondeterministic specifications in CZ language.

关键词： formal program development nondeterminism in CZ language nondeterminism in Martin-Lof's theory of types translation of CZ set theory into Martin-Lof's theory of types

来源：评论

学校读者我要写书评

暂无评论

Relation-algebraic specification and solution of special university timetabling problems

引用

JOURNAL OF LOGIC AND ALGEBRAIC programMING 2010年第8期79卷 722-739页

作者： Berghammer, Rudolf Kehden, Britta Univ Kiel Inst Informat D-24098 Kiel Germany

In this paper, we are concerned with a special timetabling problem. It was posed to us by the administration of our university and stems from the adoption of the British-American system of university education in Germany. This change led to the concrete task of constructing a timetable that enables the undergraduate education of secondary school teachers within three years in the "normal case" and within four years in the case of exceptional combinations of subjects. We develop two relation-algebraic models of the timetabling problem and in each case algorithms for computing solutions. The latter easily can be implemented in the Kiel RELVIEW tool showing that RELVIEW can be used for timetabling. (C) 2010 Elsevier Inc. All rights reserved.

关键词： Relation algebra Timetabling formal program development Tool support RELVIEW

来源：评论

学校读者我要写书评

暂无评论

Systematic parallel programming

Systematic parallel programming

引用

作者： Dingel, Juergen Carnegie Mellon University

学位级别：Ph.D.

Parallel computers have not yet had the expected impact on mainstream computing. Parallelism adds a level of complexity to the programming task that makes it very error-prone. Moreover, a large variety of very different parallel architectures exists. Porting an implementation from one machine to another may require substantial changes. This thesis addresses some of these problems by developing a formal basis for the design of parallel programs in form of a refinement calculus. The calculus allows the stepwise formal derivation of an abstract, low-level implementation from a trusted, high-level specification. The calculus thus helps structuring and documenting the development process. Portability is increased, because the introduction of a machine-dependent feature can be located in the refinement tree. development efforts above this point in the tree are independent of that feature and are thus reusable. Moreover, the discovery of new, possibly more efficient solutions is facilitated. Last but not least, programs are correct by construction, which obviates the need for difficult debugging. Our programming/specification notation supports fair parallelism, shared varia-ble and message-passing concurrency, local variables and channels. It allows the development of reactive systems, that is, possibly non-terminating programs designed to interact persistently with their environment. Moreover, the specification of liveness properties such as termination or eventual entry is supported by our methodology. The calculus rests on a compositional trace semantics that treats shared-variable and message-passing concurrency uniformly. The refinement relation combines a context-sensitive notion of trace inclusion and assumption-commitment reasoning to achieve compositionality. Most refinement rules are syntax-directed in the sense that each rule corresponds to a specific language construct. The calculus straddles both concurrency paradigms. A shared-variable program can be refined

关键词： Parallel programming systematic programming formal program development program transformation assumption-commitment reasoning trace semantics

来源：评论

学校读者我要写书评

暂无评论

A formal mapping from Object-Z specification to C plus plus code

引用

SCIENTIA IRANICA 2013年第6期20卷 1953-1977页

作者： Najafi, M. Haghighi, H. Shahid Beheshti Univ Fac Elect & Comp Engn Tehran Iran

Object-Z is an extension of Z which provides specific constructs to facilitate specification in an object-oriented style. A number of contributions have been made so far to animate Object-Z with various object-oriented programming languages. However, none of the existing animation methods present their mapping rules formally. Also, none of these animation methods prove the correctness of their mapping rules. In our previous work, we informally presented an animation method to map Object-Z specifications into C++ code. In this paper, we propose a formal mapping from Object-Z specifications to C++ code. We also prove the correctness of the given mapping rules. (C) 2013 Sharif University of Technology. All rights reserved.

关键词： formal program development Object-oriented programming Animation Object-Z C plus

来源：评论

学校读者我要写书评

暂无评论

From Object-Z specification to Groovy implementation

引用

SCIENTIA IRANICA 2018年第6期25卷 3415-3441页

作者： Zaker, F. Haghighi, H. Nazemi, E. Shahid Beheshti Univ Fac Comp Sci & Engn Tehran *** Iran

So far, valuable research studies have been conducted on mapping notations of object-oriented specification, such as Object-Z, in different object-oriented programming languages, such as C++. However, the results of selecting JVM-based programming languages for mapping have not covered most of basic Object-Z structures. In this paper, the Groovy language, as a dynamic JVM-based language, is selected to overcome some of the existing limitations. As the main contribution, the rules required for mapping Object-Z specifications to execute Groovy code are introduced. The proposed rules cover notions such as multiple inheritance, inverse specification of functions, functions defined on generic definitions, and free-type constructors. Previous methods have not covered these notions for the formal development of program from object-oriented specifications, regardless of the selected formal specification language and target programming language. In addition, in this paper, the parallel composition construct is mapped to a parallel, executable code to improve the faithfulness of the final code to the initial specification. A mapping rule for the class union construct is introduced, which has not yet been provided for any JVM-based language. Unlike previous works, instead of presenting the mapping rules in terms of natural languages, they are presented in terms of some formal mapping rules. (C) 2018 Sharif University of Technology. All rights reserved.

关键词： formal program development Object oriented programming Animation Object-Z Groovy JVM

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：