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

INFORMATION PROCESSING LETTERS 1983年第3期16卷 105-112页

作者： CONSTABLE, RL Department of Computer Science Cornell University IthacaNY 14853 USA

Logicians have known since Kleene's work in the 1940s that various kinds of constructive proofs could be compiled into executable code. The results of this variety are known for many constructive formal systems. An example can illustrate the basic ideas behind them. A very simple benchmark common in the literature, the Euclidean division algorithm, is selected. Programs are like constructive proofs of their specifications; this analogy is an exact equivalence for certain classes of programs. The relationship between formal logic and programs is a foundation for programming methodology superior to that usually adopted. Furthermore, this equivalence suggests programming languages which are much richer than all others currently in use. These claims are established through the introduction of parts of the PL/CV programming logics as a source of precision and examples.

关键词： Algorithmic logic automated logic axiomatic semantics constructive mathematics program correctness PL/CV programming logic programming methodology realizability type theory while rule

来源：评论

学校读者我要写书评

暂无评论

SUPPORTING STRUCTURED DEVELOPMENT OF COMPLEX PL-I SOFTWARE SYSTEMS

引用

SOFTWARE-PRACTICE & EXPERIENCE 1977年第2期7卷 279-293页

作者： WHITE, JR ANDERSON, RK UNIV CONNECTICUT DEPT ELECT ENGN & COMP SCISTORRSCT 06268

AbstractThe methodology of top‐down (structured) programming has emerged in the last few years as a practical approach to the problem of developing reliable software systems. The methodology, however, places certain demands on the language used for actual system implementation. In this paper we discuss the implications of these demands on a specific language, PL/I. From this discussion the basic objectives of a PL/I support system are deduced. These objectives deal primarily with: (1) specifying intermodule relationships; (2) propagating module modifications; and (3) maintaining consistency in the realization of abstractions. Finally, the essential elements of a system that realizes these objectives are describe

关键词： programming methodology Software reliability Modularization Structured programming Top‐down programming

来源：评论

学校读者我要写书评

暂无评论

CONSTRUCTIVE METHODS IN PROGRAM VERIFICATION

引用

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING 1977年第3期3卷 193-210页

作者： WEGBREIT, B XEROX CORP PALO ALTO RES CTRPALO ALTOCA 94304

Most current approaches to mechanical program verification transform a program and its specifications into first-order formulas and try to prove these formulas valid. Since the first-order predicate calculus is not decidable, such approaches are inherently limited. This paper proposes an alternative approach to program verification: correctness proofs are constructively established by proof justifications written in an algorithmic notation. These proof justifications are written as part of the program, along with the executable code and correctness specifications. A notation is presented in which code, specifications, and justifications are interwoven. For example, if a program contains a specification 3x P(x), the program also contains a justification that exhibits the particulat value of x that makes P true. Analogously, justifications may be used to state how universally quantified formulas are to be instantiated when they are used as hypotheses. Programs so justifiled may be verified by proving quantifier-free formulas. Additional classes of justifications serve related ends. Formally, justifications reduce correctness to a decidable theory. Informally, justifications establish the connection between the executable code and correctness specifications, documenting the reasoning on which the correctness is based.

关键词： Constructive Program Verification First Order Logic Instantiations Program Verification programming Language Design programming Languages programming methodology Proof Justifications Proving Programs Correct

来源：评论

学校读者我要写书评

暂无评论

DISPLAY CONDENSATION OF PROGRAM TEXT

引用

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING 1982年第5期8卷 526-529页

作者： ARCHER, J CONWAY, R CORNELL UNIV DEPT COMP SCIITHACANY 14853 STANFORD UNIV STANFORDCA 94305

In interactive systems that must display the text of programs, the size of the program is ordinarily much larger than the capacity of the screen. Although the obvious tactic is simply to select k contiguous lines for display in a k-line window, in some cases, it is helpful to be able to represent m lines in a k-line window, where m is greater than k, by condensing portions of the text. Alternative tactics for controlling such condensation are considered. The 3 systems considered - PDE1L, the Cornell Program Synthesizer, and COPE - illustrate a useful idea, as well as 2 substantially different approaches to its implementation. PDE1L and COPE are demonstrable, but user experience is limited. The Synthesizer, however, has been used for more than 2 years at numerous universities. Only extensive user experience can resolve the choice between automatic and user-controlled condensation, and it will probably be concluded that under different circumstances each of these alternatives is advantageous. The issues in general will be simply how much effort is required for user control and how well automatic condensation can deduce the user's needs and intent. Of course, the possibility of compromise also exists.

关键词： programming methodology Editing Interactive programming Prettyprinting programming Environments

来源：评论

学校读者我要写书评

暂无评论

A TECHNIQUE FOR DEVELOPING LOOP INVARIANTS

引用

INFORMATION PROCESSING LETTERS 1984年第3期18卷 137-139页

作者： REMMERS, JH Department of Mathematics and Computer Science Eastern Michigan University Ypsilanti MI 48197 U.S.A.

In order to develop a loop from a given precondition and postcondition following the method developed in Dijkstra (1976) and described in Gries (1981), one attempts to obtain a loop invariant by weakening the postcondition in some way. To do so, one standard technique is to replace a constant or expression that occurs in the postcondition by a fresh variable. A situation in which it is useful to introduce fresh variables to replace some of the occurrences of existing variables is discussed. Both a new algorithm for linear search and an algorithm for binary search to illustrate the technique are developed.

关键词： Invariant relation loop invariant programming methodology

来源：评论

学校读者我要写书评

暂无评论

INITIALIZING ALGORITHMS - NOTE TO THE ARTICLE COMPUTER METHODS FOR SAMPLING FROM GAMMA-DISTRIBUTION, BETA-DISTRIBUTION, POISSON-DISTRIBUTION AND BINOMIAL-DISTRIBUTION

引用

COMPUTING 1979年第2期22卷 185-189页

作者： APOSTOLOPOULOS, N SCHUFF, G Institut für Quantitative Ökonomik und Statistik Fachrichtung Angewandte Statistik Freie Universität Berlin Corrensplatz 2 D-1000 Berlin 33

A general initialization principle is presented that increases the efficiency of algorithms in terms of computation time. It is applied to the algorithm NS in [1] and results in significant performance improvements. I... 详细信息

关键词： Random numbers pseudorandom binomial distributions simulation algorithm interfaces programming methodology

来源：评论

学校读者我要写书评

暂无评论

DATALOGY - THE COPENHAGEN TRADITION OF COMPUTER-SCIENCE

引用

BIT 1988年第3期28卷 450-472页

作者： SVEINSDOTTIR, E FROKJAER, E UNIV COPENHAGEN INST DATALOGDK-2100 COPENHAGEN ODENMARK ROSKILDE UNIV CTR DATALOG AFDELINGDK-4000 ROSKILDEDENMARK

Since the middle of the 1960s, computer science has been practised in Denmark under Peter Naur's termdatalogy, the science of data processes. Starting at Regenecentralen and the University of Copenhagen, the Copenhagen Tradition of Computer Science has developed its own special characteristics by means of a close connection with applications and other fields of knowledge. The tradition is not least visible in the area of education. Comprehensive project activity is an integral part of the curriculum, thus presenting theory as an aspect of realistic solutions known primarily through actual experience. Peter Naur early recognized the particular educational challenges presented by computer science. His innovations have shown their quality and vitality also at other universities. There is a close connection between computer science training as it has been formed at Copenhagen University, and the view of computer science which has characterized Peter Naur's research. We illustrate how the study of programming and system development conceived as a human activity has been an all-pervasive theme in Naur's work. This approach has set the scene for central research issues in software development which today seem more topical than ever.

关键词： K.3 A0 D0 computer science education and training computer science datalogy programming methodology software engineering Peter Naur history

来源：评论

学校读者我要写书评

暂无评论

A DESIGN METHOD FOR EMBEDDED SOFTWARE SYSTEMS

引用

BIT 1988年第3期28卷 427-438页

作者： RAVN, AP RISCHEL, H LOVENGREEN, HH TECH UNIV DENMARK DEPT COMP SCIDK-2800 LYNGBYDENMARK

A method for design of embedded real-time systems is described. We discuss how the method separates concerns and at what points theory is applied. We also report on our experience from teaching the method to engineers... 详细信息

关键词： C.3 D.2.2 programming methodology Software Engineering Embedded Real-time Systems

来源：评论

学校读者我要写书评

暂无评论

Teaching of programming with a programmer's theory of programming

Teaching of programming with a programmer's theory of progra...

引用

Conference on Informatics Curricula, Teaching Methods and Best Practice

作者： Reinfelds, J New Mexico State Univ Klipsch Sch EE & C Las Cruces NM 88003 USA

ISBN: (纸本)140207266X

We review the introductory programming courses of the widely accepted Curricula '68, '78, '1991 and '2001. We note that a one-language, imperative-paradigm approach still prevails, although multi-language programming systems are already available. We discuss the Kernel Language Approach, which provides a programmer's theory of programming that permits a widening of introductory courses to multi-language, multi-thread programming without loss of depth. We suggest two broad outlines for the removal of the one-language constriction from introductory programming courses. We observe that because of the introduction of dotNET and because of student exposure to net-centric multimedia applications, text-based "Hello World!" examples disappoint the expectations of today's students.

关键词： programming methodology programming courses curriculum computer science software engineering introductory courses

来源：评论

学校读者我要写书评

暂无评论

Achievements in answer set programming

引用

THEORY AND PRACTICE OF LOGIC programming 2017年第5-6期17卷 961-973页

作者： Lifschitz, Vladimir Univ Texas Austin Austin TX 78712 USA

This paper describes an approach to the methodology of answer set programming that can facilitate the design of encodings that are easy to understand and provably correct. Under this approach, after appending a rule or a small group of rules to the emerging program, we include a comment that states what has been "achieved" so far. This strategy allows us to set out our understanding of the design of the program by describing the roles of small parts of the program in a mathematically precise way.

关键词： answer set programming teaching logic programming programming methodology

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：