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

PROGRAM-DEVELOPMENT BY INDUCTIVE STEPWISE REFINEMENT

SOFTWARE-PRACTICE & EXPERIENCE 1985年第1期15卷 1-28页

作者： DROMEY, RG Department of Computing Science University of Wollongong P.O. Box 1144 Wollongong N.S.W. 2500 Australia

A constructive method of program development is presented. It seeks to unify two important ideas about program development. Namely that programming is a goal-oriented activity and that there should be a correspondence between data and program structures. The latter concept is seen to be extensible beyond the data processing context in which it was originally proposed. Induction provides the vehicle for program development by stepwise refinement, with the final program being constructed by application of a sequence of progressively more powerful generalizations. The design process employed guarantees the correctness of the final program provided that each of the refinement steps have been correctly taken. The method is illustrated by a number of samples.

关键词： Program development Inductive stepwise refinement Structure clashes Induction Orienting mechanism Post-condition Syntax diagrams programming methodology

来源：评论

学校读者我要写书评

暂无评论

A methodology FOR DEVELOPING DISTRIBUTED PROGRAMS

引用

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING 1987年第8期13卷 967-976页

作者： RAMESH, S MEHNDIRATTA, SL Department of Computer Science and Engineering Indian Institute of Technology

A methodology for constructing distributed programs is presented that is different from existing methodologies. It is based on the well-known notion of developing distributed programs via synchronous and centralized programs. The distinguishing features of the methodology are: 1. Specification includes process structure data, and distributed programs are developed taking this information into account. 2. A new class of programs, called programs with processes involving shared actions, is employed in the development process. 3. A transformational approach is suggested to solve the problems inherent in the method of developing distributed programs through synchronous and centralized programs. The proposed methodology has been applied to many standard problems and found to be very useful.

关键词： Program Transformation Communicating Processes Decentralization Distributed programming programming methodology

来源：评论

学校读者我要写书评

暂无评论

Datatype-Generic Termination Proofs

引用

THEORY OF COMPUTING SYSTEMS 2008年第3-4期43卷 362-393页

作者： Backhouse, Roland Doornbos, Henk Univ Nottingham Sch Comp Sci & Informat Technol Nottingham NG8 1BB England Questance NL-9711 TS Groningen Netherlands

Datatype-generic programs are programs that are parameterised by a datatype. We review the allegorical foundations of a methodology of designing datatype-generic programs. The notion of F-reductivity, where F parametrises a datatype, is reviewed and a number of its properties are presented. The properties are used to give concise, effective proofs of termination of a number of datatype-generic programming schemas. The paper concludes with a concise proof of the well-foundedness of a datatype-generic occurs-in relation.

关键词： Datatype Generic programming Relation algebra Allegory programming methodology

来源：评论

学校读者我要写书评

暂无评论

EMERALD - A GENERAL-PURPOSE programming LANGUAGE

引用

SOFTWARE-PRACTICE & EXPERIENCE 1991年第1期21卷 91-118页

作者： RAJ, RK TEMPERO, E LEVY, HM BLACK, AP HUTCHINSON, NC JUL, E DIGITAL EQUIPMENT CORP CAMBRIDGE RES LABCAMBRIDGEMA 02139 UNIV ARIZONA DEPT COMP SCITUCSONAZ 85721 UNIV COPENHAGEN DIKUDK-2100 COPENHAGENDENMARK

Emerald is a general-purpose language with aspects of traditional object-oriented languages, such as Smalltalk, and abstract data type languages, such as Modula-2 and Ada. It is strongly typed with a nontraditional object model and type system that emphasize abstract types, allow separation of typing and implementation, and provide the flexibility of polymorphism and subtyping with compile-time checking. This paper describes the Emerald language and its programming methodology. We give examples that demonstrate Emerald's features, and compare and contrast the Emerald approach to programming with the approaches used in other similar languages.

关键词： programming LANGUAGES programming methodology OBJECT-ORIENTED programming ABSTRACT DATA TYPES INHERITANCE OBJECT-BASED CONCURRENCY

来源：评论

学校读者我要写书评

暂无评论

HIGHER-ORDER COMMUNICATIONS FOR CONCURRENT programming

引用

PARALLEL COMPUTING 1984年第3-4期1卷 331-336页

作者： PETTOROSSI, A SKOWRON, A UNIV N CAROLINA DEPT MATHCHARLOTTENC 28223

In Pettorossi and Skowron (1983) a recursive-equations language is introduced. Its operational semantics is specified by means of computing agents which communicate and exchange messages. Those communications are, so to speak, zero-order, in the sense that the exchanged messages are values of a data structure, possibly defined by the programmer. In this paper we extend that approach and we consider also ‘higher-order’ communications by allowing the exchange of agents behaviours, i.e. sets of computations, among computing agents. This extension leads to a new programming methodology which makes use of proofs of computing agents behaviours and their related strategies.

关键词： programming methodology higher-order communications concurrent programming computing agents

来源：评论

学校读者我要写书评

暂无评论

Automated verification of weak equivalence within the SMODELS system

引用

THEORY AND PRACTICE OF LOGIC programming 2007年第6期7卷 697-744页

作者： Janhunen, Tomi Oikarinen, Emilia Aalto Univ Dept Comp Sci & Engn Lab Theoret Comp Sci FIN-02150 Espoo Finland

In answer set programming (ASP), a problem at hand is solved by (i) writing a logic program whose answer sets correspond to the solutions of the problem, and by (ii) computing the answer sets of the program using an answer set solver as a search engine. Typically, a programmer creates a series of gradually improving logic programs for a particular problem when optimizing program length and execution time on a particular solver. This leads the programmer to a meta-level problem of ensuring that the programs are equivalent, i.e., they give rise to the same answer sets. To case answer set programming at methodological level, we propose a translation-based method for verifying the equivalence of logic programs. The basic idea is to translate logic programs P and Q under consideration into a single logic program EQT(P,Q) whose answer sets (if such exist) yield counter-examples to the equivalence of P and Q. The method is developed here in a slightly more general setting by taking the visibility of atoms properly into account when comparing answer sets. The translation-based approach presented in the paper has been implemented as a translator called LPEQ that enables the verification of weak equivalence within the SMODELS system using the same search engine as for the search of models. Our experiments with LPEQ and SMODELS suggest that establishing the equivalence of logic programs in this way is in certain cases much faster than naive cross-checking of answer sets.

关键词： answer set programming weak equivalence programming methodology program optimization

来源：评论

学校读者我要写书评

暂无评论

THEORY OF MODULES

引用

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING 1987年第7期13卷 820-829页

作者： GANNON, JD HAMLET, RG MILLS, HD UNIV MARYLAND INST ADV COMP STUDIESCOLLEGE PKMD 20742 OREGON GRAD CTR DEPT COMP SCI & ENGNBEAVERTONOR 97006 IBM CORP BETHESDAMD 20817

Because large-scale software development is a struggle against internal program complexity, the modules into which programs are separated play an important role in software engineering. A module that encapsulates a data type permits the programmer to ignore both the details of its operations and of its value representations. It is a primary strength of program proving that, as modules divide a program and make it easier to understand, so do they divide its proof. Each module can be verified in isolation, then its internal details can be ignored in a proof of its use. Proofs of module abstractions that are based on functional semantics are described and, this is contrasted with the Alphard formalism based on Hoare logic.

关键词： Program Verification Abstract Data Types Functional Semantics Modules programming methodology Program Specifications

来源：评论

学校读者我要写书评

暂无评论

The joy of formula manipulation

引用

INFORMATION PROCESSING LETTERS 2001年第2-4期77卷 89-96页

作者： Feijen, WHJ Eindhoven Univ Technol Dept Math & Comp Sci NL-5600 MB Eindhoven Netherlands

In mathematical circles, there is the overall opinion that formulae, in their capacity of syntactic units, are dead things, and that formula manipulation tears the heart out of mathematics. In these circles, formulae largely live by virtue of what they stand for, of what they mean, of how they feel and appeal to our intuition-our(?) intuition? And their meanings then tell which formulae to consider next. Poor Leibniz, poor Lagrange, poor Boole, poor Hilbert, and all others who shifted their attention towards uninterpreted formulae manipulation: they were all wrong, weren't they? Oh, and poor we, Edsger W. Dijkstra and all those programmers who converted themselves to formulae manipulators, because their profession demanded it. (This cultural gap in doing mathematics was once expressed quite aptly by Dijkstra when he remarked, "Ik hou van wiskunde, maar spaar me de mathematen". [''I love mathematics, but it's the mathematicians I cannot stand'.]) Well, our profession of programming demanded a conscious and active engagement in formula manipulation and therefore we entered that field of endeavour;and we learned how mighty and powerful, how prosperous and effective, and how indicative of designing this change in attitude turned out to be, not only for the benefit of programming, but for vast parts of mathematics as well. And moreover, we learned to enjoy the activity. In this note we try to convey the effectiveness and joy of formula manipulation through a small number of simple examples from both mathematics and programming. (C) 2001 Elsevier Science B.V. All rights reserved.

关键词： programming methodology calculational reasoning

来源：评论

学校读者我要写书评

暂无评论

Regular algebra applied to language problems

引用

JOURNAL OF LOGIC AND ALGEBRAIC programming 2006年第2期66卷 71-111页

作者： Backhouse, R Univ Nottingham Sch Comp Sci & Informat Technol Nottingham NG8 1BB England

Many functions on context-free languages can be expressed in the form of the least fixed point of a function whose definition mimics the grammar of the given language. Examples include the function returning the length of the shortest word in a language, and the function returning the smallest number of edit operations required to transform a given word into a word in a language. This paper presents the basic theory that explains when a function on a context-free language can be defined in this way. It is shown how the theory can be applied in a methodology for programming the evaluation of such functions. Specific results include a novel definition of a regular algebra focusing on the existence of so-called "factors", and several constructions of non-trivial regular algebras. Several challenging problems are given as examples, some of which are old and some of which are new. (c) 2005 Elsevier Inc. All rights reserved.

关键词： galois connection fixed point programming methodology problem generalisation factor theory factor matrix path-finding language inclusion

来源：评论

学校读者我要写书评

暂无评论

INSITU INVERSION OF A CYCLIC PERMUTATION

引用

INFORMATION PROCESSING LETTERS 1987年第1期24卷 11-14页

作者： FEIJEN, WHJ VANGASTEREN, AJM GRIES, D CORNELL UNIV DEPT COMP SCIITHACANY 14853

Algorithms that deal with arrays in a complicated fashion are either explained informally in terms of pictures, explained more formally but with overwhelming details, or not explained at all. An attempt is made to present some notations and concepts to make the development and proof of one such algorithm more appealing and convincing. The algorithm is developed for the in-situ inversion of a cyclic permutation represented in an array. The ring is introduced as a suitable representation of a cyclic permutation since conventional representations of cyclic permutations are not suited to manipulative needs. For the sake of manageability, few elements of rings should have a name, in contrast to the conventional notations for rings in which each element is named and in which even a simple rule becomes awkward to formulate. The exercise confirms that, in designing algorithms, the development of adequate mathematical notations is a key issue that is hardly addressed by traditional mathematics.

关键词： programming methodology program development in-situ inversion

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：