首页/论文/1507.00723

arXiv 1507.007232015-07cs.PLcs.SE

程序论

Theory of Programs

Bertrand Meyer

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

摘要英文摘要相关论文

摘要：

从初等集合论的一些概念建立起来的程序、程序设计和程序设计语言的一般理论。作为定理，导出被经典编程方法视为公理的性质。涵盖顺序和并发计算。

英文摘要：

A general theory of programs, programming and programming languages built up from a few concepts of elementary set theory. Derives, as theorems, properties treated as axioms by classic approaches to programming. Covers sequential and concurrent computation.

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

阅读原文

阅读 PDF ↗

arXiv 页面 ↗HTML 原文 ↗

本文内容

摘要英文摘要相关论文

机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。

继续探索

相关论文

具有多线程和副作用的初等仿射$lambda$-演算

Elementary affine $lambda$-calculus with multithreading and side effects

线性逻辑提供了一个框架来控制高阶函数程序的复杂性。我们提出了一个扩展这个框架的程序与多线程和副作用的情况下，小学时间为重点。我们的主要贡献如下。首先，我们提供了一个新的组合证明终止在初等时间的功能的情况下。其次，我们开发了一个扩展的方法，以调用的值$lambda$-演算多线程和副作用。第三，我们引入了一个基本的仿射型系统，保证标准的主题约简和进步属性。最后，我们说明了规划的迭代函数的副作用所提出的形式主义。

2011-06-10cs.PL

对使用初等函数的程序进行声音近似

Sound Approximation of Programs with Elementary Functions

MPI-SWS（马克斯·普朗克计算机研究所）；Univ Lyon, Inria, CNRS, ENS de Lyon, Université Claude Bernard Lyon 1, LIP UMR 5668（里昂大学、法国国家信息与自动化研究所、法国国家科学研究中心、里昂高等师范学校、里昂第一大学、LIP实验室）

本文提出了一种自动化方法和工具，用于在小型程序中近似初等函数调用，同时保证用户提供的误差界。该工具利用现有的舍入误差计算和单个初等函数调用近似的技术，并提供自动选择多个参数的功能。实验表明，通过牺牲但保证的准确性，可以实现显著的效率提升。

2018-11-26cs.MScs.NAcs.PL

超越代数数据类型上程序不变量的初等表示

Beyond the Elementary Representations of Program Invariants over Algebraic Data Types

一阶逻辑是表达计算属性的一种自然方式。它传统上用于各种程序逻辑中，用于表示正确性属性和证书。虽然这样的表示是表达一些理论，他们无法表达代数数据类型（ADT）的许多有趣的属性。在本文中，我们探讨了三种不同的方法来表示ADT操作程序的程序不变量：树自动机，和一阶公式有或没有大小限制。我们比较这些表示的表达能力，并证明了负的可定义性的一阶表示使用泵引理。我们提出了一种方法来自动推断ADT操作程序的程序不变量减少到一个有限的模型发现者。被称为RInGen的实现已被评估对国家的最先进的不变合成器，并已被实验证明是有竞争力的。特别是，由自动机表示的程序不变量能够表达更复杂的计算属性，并且它们的自动构造通常成本较低。

2021-04-14cs.FLcs.PL

程序分析

Program Analysis (an Appetizer)

这本书是对程序分析的介绍，它比我们的高级书籍《程序分析原理》（施普林格，2005）要初级得多。这本书没有使用流程图作为程序的模型，而是遵循我们的介绍性书籍Formal Methods an Appetizer（Springer，2019），使用程序图作为程序的模型。根据我们的经验，这使得我们的计算机科学和计算机工程专业的学生在丹麦技术大学的硕士课程02242：程序分析中更容易获得基本思想。在这里，我们逐渐用本书中的材料取代了对《程序分析原理》中更基本部分的使用。

2020-12-18cs.PL

pun：属性之趣；迈向一种内置程序验证设施的编程语言

pun: Fun with Properties; Towards a Programming Language With Built-in Facilities for Program Validation

本文提出并形式化了一种内置属性验证机制的函数式编程语言 pun，通过自动生成输入数据降低基于属性测试的准入门槛，并在二叉搜索树库上验证了其有效性。

2023-09-12cs.PL

具有内建和聚集的逻辑程序的求值：一种包关系演算

Evaluation of Logic Programs with Built-Ins and Aggregation: A Calculus for Bag Relations

我们提出了一个计划，用于翻译逻辑程序，这可能会使用聚合和算术，代数表达式表示袋关系的Herbrand宇宙的地面条款。为了评估这些关系的查询，我们开发了一个操作语义的基础上长期重写的代数表达式。这种方法可以利用算术恒等式并恢复一系列有用的策略，包括延迟工作直到它变得可能或必要的懒惰策略。

2020-10-20cs.PLcs.SC

更多相关论文收起更多论文

关联数组程序的数据流分析

Data-flow Analysis of Programs with Associative Arrays

动态规划语言（如PHP、JavaScript和Python）提供内置的数据结构，包括关联数组和具有类似语义的对象-对象属性可以在运行时创建并通过任意表达式访问。虽然以这些语言编写的应用程序的高级别安全性和安全性可能特别重要（考虑存储敏感数据并在全球范围内提供其功能的Web应用程序），但动态数据结构对数据流分析提出了重大挑战，使得传统的静态验证方法既不可靠又不精确。在本文中，我们提出了一个健全的和精确的方法，值和点的分析程序与关联数组类数据结构，数据流分析可以建立在。我们在一个web应用程序域中实现了我们的方法-在一个PHP代码分析器中。

2014-05-06cs.PLcs.SE

Array-OL的初等变换分析

Elementary transformation analysis for Array-OL

Array-OL是一种高级规约语言，专用于定义密集型信号处理应用。存在用于将Array-OL规范实现为数据并行程序的若干工具。虽然Array-OL可以直接使用，但从应用程序的顺序版本中推导出部分规范通常很方便。本文提出了这样的分析，并探讨其可行性和局限性。

2007-05-22cs.PL

计算思维的智能评估和辅导MOOC使用MindReader

Smart Assessment of and Tutoring for Computational Thinking MOOC Assignments using MindReader

计算机程序的自动语义理解的主要障碍之一是缺乏关于什么构成代码段的功能等价的知识。我们假设，一个健全的知识库可以用来演绎理解代码段的层次结构的方式，首先解构代码，然后从基本知识和等价规则的基本代码段重建。该方法也可以被设计为从概念和抽象算法作为反函数产生可计算程序。在本文中，我们介绍了MindReader在线评估系统背后的核心思想，该系统能够理解学生在入门级编程课程（如Java，C++和Python）中学习的各种基本算法。MindReader系统能够评估学生的作业，并指导他们如何在没有人工帮助的情况下实时的开发正确和更好的代码。

2017-04-17cs.PL

Pyro：深度通用概率编程

Pyro: Deep Universal Probabilistic Programming

Uber AI Labs（优步人工智能实验室）；Uber Technologies, Inc.（优步科技公司）；Stanford University（斯坦福大学）

Pyro是一种基于Python的概率程序设计语言，作为在AI研究中开发高级概率模型的平台。为了扩展到大型数据集和高维模型，Pyro使用基于PyTorch（一种现代GPU加速的深度学习框架）的随机变分推理算法和概率分布。为了适应复杂或特定于模型的算法行为，Pyro利用Poutine，这是一个用于修改概率程序行为的可组合构建块库。

2018-10-18cs.LGcs.PLstat.ML

一种新的面向上下文程序模型

A new model for Context-Oriented Programs

面向上下文编程（COP）是一种新的编程技术，它允许在程序执行时更改命令执行的上下文。与面向对象编程（面向方面编程）相比，COP更灵活（模块化和结构化）。本文提出了一个精确的语法导向的操作语义面向上下文的编程与层，实现COP语言，如ContextJ* 和ContextL。我们的语言模型是建立在Java丰富的层概念和激活和停用层范围。本文还提出了一个静态类型系统，保证类型化的程序不会卡住。利用所提出的语义方法，本文给出了类型系统的数学正确性。

2014-02-23cs.PLcs.SE

图重写系统的策略规划

Strategic programming on graph rewriting systems

我们描述了一种策略语言来控制图重写规则的应用，并展示了如何使用这种语言来编写高级声明式程序在几个应用领域。这种语言是基于图的编程工具的一部分，内置于端口图转换和可视化环境PORGY中。

2010-12-27cs.PL

概率规划中的条件作用

Conditioning in Probabilistic Programming

我们调查的语义复杂性的条件，概率规划的一个主要特点。我们提供了一个最弱的（自由）前置条件（w（l）p）的基本概率程序设计语言pGCL扩展条件的语义。我们证明了定量最弱（自由）的先决条件与条件（自由）期望回报的马尔可夫链，并表明语义条件是一个真正的保守扩展。我们提出了两个程序转换，完全消除任何程序的条件，并证明其正确性使用的w（l）p-语义。最后，我们展示了如何的w（l）p-语义可以用来确定条件概率的参数匿名协议，并表明，一个归纳的w（l）p-语义的条件在非确定性的概率程序不存在。

2015-04-01cs.PL

使用FastFlow和自卸载加速顺序程序

Accelerating sequential programs using FastFlow and self-offloading

FastFlow是一个专门针对高速缓存一致性共享内存多核的编程环境。FastFlow是作为一个C++模板库堆栈实现的，它构建在无锁（无栅栏）同步机制之上。在本文中，我们提出了FastFlow的进一步发展，使程序员能够在未使用的CPU上运行的动态创建的软件加速器上卸载部分工作负载。卸载的函数可以很容易地从预先存在的顺序代码中派生出来。我们特别强调的有效权衡人类生产力和执行效率的方法。

2010-02-25cs.DCcs.PLcs.SE

上世纪80年代的BASIC编程教科书能教给我们什么？

What can a 1980s BASIC programming textbook teach us today?

Elementary Basic出版于1982年，是一本介绍性的编程文本，其中有一个新颖的中心思想，即虚构的19世纪侦探夏洛克·福尔摩斯使用计算机来帮助解决谜团。它也是新颖的同类书籍的时间，其重点是程序设计。在其他方面，例如它使用BASIC语言，它代表了它的时代。在它被写了35年之后，我认为值得回顾它，看看今天仍然有什么意义，以及会有什么不同的做法。我们今天甚至可以学到一些关于编程教学的东西。特别令人感兴趣的是BASIC语言的使用对本书内容的影响程度。

2020-12-30cs.PL

编程确实是简单的数学

Programming Really Is Simple Mathematics

本文基于初等集合论，以零公理方式重构编程基础，用三种操作和子集操作符定义规格、程序及正确性，推导出经典编程定律并机械验证。

2025-02-27cs.LOcs.PLcs.SE

标准ML中的反应式编程

Reactive Programming in Standard ML

反应式系统是保持与其环境的持续交互的系统，通过从环境接收输入事件并产生输出事件作为响应来激活。设计用于对这样的系统进行编程的现代程序设计语言使用基于瞬时和激活的概念的范例。我们描述了一个标准ML的库，它为编程反应式系统提供了基本的原语。该库是一个低级系统，可以在其上构建更复杂的反应行为，这为现有反应语言的原型扩展提供了一个方便的框架。

2004-05-23cs.PL

CISE3：Verificação de aplicaçées com consistência fraca em Why3

CISE3: Verificação de aplicações com consistência fraca em Why3

在这篇文章中，我们提出了一个工具，用于验证建立在顶级复制数据库上的程序。该工具评估顺序规范，并推断哪些操作需要同步，以便程序在分布式环境中正常运行。我们的原型是建立在演绎验证平台Why3。Why3框架提供了一个复杂的用户体验，扩展到现实案例研究的可能性，以及高度的自动化。一个案例研究和讨论，实验验证我们的方法的目的。

2019-09-09cs.LOcs.PL

由初等推理系统定义的计算的语义性质

Semantic Properties of Computations Defined by Elementary Inference Systems

该研究针对初等推理系统定义的计算的语义性质，提出借助其任意一阶模型的可满足性来（否）证性质的方法，可应用于编程语言及重写系统等的性质分析。

2025-10-30cs.LOcs.PLcs.SC

ALEA IACTA EST：一种用于可人工执行的随机实验的声明式领域特定语言

ALEA IACTA EST: A Declarative Domain-Specific Language for Manually Performable Random Experiments

提出一种名为 Alea 的声明式领域特定语言，用于规范可人工执行的随机实验，支持静态分析概率分布和模拟执行，面向非专业程序员，设计实现仍在进行中。

2025-08-06cs.PLmath.PR