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

RECURSIVE-PROGRAMS AS DEFINITIONS IN 1ST ORDER logic

SIAM JOURNAL ON COMPUTING 1984年第2期13卷 374-408页

作者： CARTWRIGHT, R Rice Univ Computer Science Program Houston TX USA Rice Univ Computer Science Program Houston TX USA

Despite the reputed limitations of first order logic, it is easy to state and prove almost all interesting properties of recursive programs within a simple first order theory, by using an approach we call “first order programming logic”. Unlike higher order logics based on fixed-point induction, first order programming logic is founded on deductive principles that are familiar to most programmers. Informal structural induction arguments (such as termination proofs for LISP append, McCarthy’s 91-function, and Ackermann’s function) have direct formalizations within the system.

关键词： programming logic recursive programs recursive definitions rewrite rules semantics verification program transformations

来源：评论

学校读者我要写书评

暂无评论

A RIGOROUS APPROACH TO FAULT-TOLERANT programming

引用

IEEE TRANSACTIONS ON SOFTWARE ENGINEERING 1985年第1期11卷 23-31页

作者： CRISTIAN, F UNIV NEWCASTLE UPON TYNE NEWCASTLE TYNE NE1 7RUTYNE & WEARENGLAND

The design of programs that are tolerant of hardware fault occurrences and processor crashes is examined. Using a stable storage management system as a running example, a new approach is presented for specifying, understanding, and verifying the correctness of fault-tolerant software. The approach extends earlier developed axiomatic reasoning techniques to the design of fault-tolerant systems by modeling hardware faults as being operations that are performed at random time intervals on any computing system by the system's adverse environment. A clear distinction is made between the concepts of software correctness and system reliability in the face of hardware malfunction. Fault hypotheses are specified axiomatically and design correctness is proven by employing a programming logic extended with fault axioms and rules. Stochastic modeling is used to verify reliability/availability system attributes. The combined correctness and reliability verifications establish that, under given fault and reliability hypotheses, a system behaves according to its functional specifications with a probability greater than prescribed by its reliability specifications.

关键词： Stochastic Modeling Availability Correctness Fault Tolerance programming logic Reliability

来源：评论

学校读者我要写书评

暂无评论

Rapid prototyping for pervasive applications

引用

IEEE PERVASIVE COMPUTING 2007年第2期6卷 76-84页

作者： Weis, Torben Knoll, Mirko Ulbrich, Andreas Muehl, Gero Brandle, Alexander Univ Stuttgart D-7000 Stuttgart Germany Tech Univ Berlin D-1000 Berlin Germany

VisualRDK is a high-level programming language for prototyping pervasive applications. Context is tightly integrated into the language itself, so developers can attach functionality to locations, persons, or situation... 详细信息

关键词： Debugging Prototype Context Aware Application logic programming logic

来源：评论

学校读者我要写书评

暂无评论

Strength Induction in a Haskell Program Verifier

引用

ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE 2007年 193卷 61-79页

作者： Kieburtz, Richard B. Portland State Univ Portland OR 97201 USA

Haskell employs a melange of strict and non-strict evaluation semantics, hence a Haskell verifier should be capable of checking assumptions that program variables may or may not denote well-defined values. The paper introduces a new strategy, called strength induction, that supports automatic checking of definedness assumptions. Strength induction has been implemented in Plover, an automated property-verifier for Haskell programs that has been under development for the past three years as a component of the Programatica project. In Programatica, predicate definitions and property assertions written in P-logic, a programming logic for Haskell, can be embedded in the text of a Haskell program module. Properties refine the type system of Haskell but cannot be verified by type-checking alone;a more powerful logical verifier is required. Plover codes the proof rules of P-logic, and additionally, embeds strategies and decision procedures for their application and discharge. It integrates a reduction system that implements a rewriting semantics for Haskell terms with a congruence-closure algorithm that supports reasoning with equality.

关键词： Haskell automatic verification programming logic rewriting strategies Stratego reduction normal forms theorem proving structure splitting strength induction lazy evaluation strictness

来源：评论

学校读者我要写书评

暂无评论

PROGRAMS AS PROOFS - A SYNOPSIS

引用

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

来源：评论

学校读者我要写书评

暂无评论

A formal nethod (a networked formal method)

引用

INNOVATIONS IN SYSTEMS AND SOFTWARE ENGINEERING 2010年第4期6卷 255-268页

作者： Breuer, Peter T. Pickin, Simon Univ Birmingham Dept Comp Sci Birmingham W Midlands England Univ Carlos III Dept Ing Telemat Madrid Spain

A year-long trial has seen a large lightweight verification problem treated by an ad hoc distributed network of identical solvers. The trialled problem is the semantic analysis of the C code in the Linux kernel to exclude a common deadlock possibility. The aim of the programme behind the experiment is to develop a viable loosely coupled distributed formal method which a community of interested part-time helpers on the net can lend their computing cycles to as they will, or send their own verification problems to for solving.

关键词： Formal methods programming logic Static analysis Linux kernel C Open source Distributed programming

来源：评论

学校读者我要写书评

暂无评论

TERMINATING GENERAL RECURSION

引用

BIT 1988年第3期28卷 605-619页

作者： NORDSTROM, B CHALMERS UNIV TECHNOL DEPT COMP SCIS-41296 GOTHENBURGSWEDEN GOTHENBURG UNIV S-41296 GOTHENBURGSWEDEN

In Martin-L?f's type theory, general recursion is not available. The only iterating constructs are primitive recursion over natural numbers and other inductive sets. The paper describes a way to allow a general recursion operator in type theory (extended with propositions). A proof rule for the new operator is presented. The addition of the new operator will not destroy the property that all well-typed programs terminate. An advantage of the new program construct is that it is possible to separate the termination proof of the program from the proof of other properties.

关键词： D.2.1 D.2.4 D.3.1 F.3.1 F.3.3 recursion well-founded induction programming logic fixed point termination proof

来源：评论

学校读者我要写书评

暂无评论

Semantics and logic of object calculi

引用

THEORETICAL COMPUTER SCIENCE 2004年第1-3期316卷 191-213页

作者： Reus, B Streicher, T Univ Sussex Dept Informat Brighton E Sussex England Tech Univ Darmstadt Fachbereich Math D-64287 Darmstadt Germany

The main contribution of this paper is a formal characterization of recursive object specifications and their existence based on a denotational untyped semantics of the object calculus. Existence is not guaranteed but can be shown employing Pitts' results on relational properties of domains. The semantics can be used to analyse and verify Abadi and Leino's object logic but it also suggests extensions. For example, specifications of methods may not only refer to fields but also to methods of objects in the store. This can be achieved without compromising the existence theorem. An informal logic of predomains is in use intentionally in order to avoid any commitment to a particular syntax of specification logic. (C) 2004 Elsevier B.V. All rights reserved.

关键词： object logic programming logic program verification denotational semantics domain theory

来源：评论

学校读者我要写书评

暂无评论

Analogy Mapping for Different Learning Style of Learners in programming 3

Analogy Mapping for Different Learning Style of Learners in ...

引用

3rd International Conference on Science in Information Technology (ICSITech)

作者： Sukamto, Rosa Ariani Megasari, Rani Univ Pendidikan Indonesia Comp Sci Educ Dept Bandung Indonesia

ISBN: (纸本)9781509058662

programming logic is often hard to understand for novice, but in the other side, programming is one of the most important subjects in computer science program. Analogy Mapping is a media which converts source code to analogies images using state machine in order to help students understanding programming logic easily. Therefore this paper reports our work about the effectivity of Analogy Mapping in learning process for basic programming subject students with different learning style.

关键词： programming learner programming logic logic thinking Analogy Analogy Mapping

来源：评论

学校读者我要写书评

暂无评论

Prize-Based Learning in an Introductory Computer Course-A Case Study

引用

EUROPEAN JOURNAL OF EDUCATION 2024年第4期59卷

作者： Vogel, Joyce Bouhnik, Dan Jerusalem Coll Technol Dept Comp Sci & Software Engn Jerusalem Israel Jerusalem Coll Technol Jerusalem Israel

Introduction to Computer Science is traditionally the first course that all computer science and software engineering majors take. The course introduces many problem-solving techniques which can be challenging for many freshman students. In order to mitigate some of the issues of this course, we, at the Higher Education Institute, introduced a new prerequisite course, Introduction to programming logic, which is a required course for all students who have not taken any previous computer science course. In the Summer Session of 2022, we included prize-based learning in one of the sections of the course. Prize-based learning is similar to both problem-based learning and project-based learning in many aspects, including the principle of student-centred learning. However, it differs with respect to the motivation for student success. This approach utilises the students' ambition to win, to encourage students to work harder and learn more both inside as well as outside the classroom.

关键词： higher education introduction to computer science prize-based learning programming logic

来源：评论

学校读者我要写书评

暂无评论

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

请选择保存的检索档案：

请选择收藏分类：

通借通还

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

时间限定

文献类型

馆藏选择

核心期刊

语言

文献类型

帮助

文字说明：

检索规则说明：

检索范例：

分类表

所选分类

限定检索结果

文献类型

馆藏范围

日期分布

学科分类号

主题

机构

作者

语言

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

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

通借通还

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

请选择保存的检索档案：

请选择收藏分类：