We consider Hoare-style verification for the graph programming language GP 2. In previous work, graph properties were specified by so-called E-conditions which extend nested graph conditions. However, this type of assertions is not easy to comprehend by programmers that are used to formal specifications in standard first-order logic. In this paper, we present an approach to verify GP 2 programs with a standard first-order logic. We show how to construct a strongest liberal postcondition with respect to a rule schema and a precondition. We then extend this construction to obtain strongest liberal postconditions for arbitrary loop-free programs. Compared with previous work, this allows to reason about a vastly generalised class of graph programs. In particular, many programs with nested loops can be verified with the new calculus.


翻译:我们考虑Hoare 式的图形编程语言 GP 2. 在先前的工作中,图形属性是由所谓的电子条件确定的,这些条件延长了嵌套的图形条件。 但是,这种类型的断言不容易被程序员理解,而程序员在标准一阶逻辑中用于正式的规格。 在本文中,我们提出一种方法,用标准一阶逻辑来核查GP 2程序。我们展示了如何在规则模式和前提条件方面建立一个最强有力的自由后设条件。 然后我们扩展了这一构思,以获得任意无环程序最有力的自由后设条件。 与先前的工作相比, 这可以解释一个非常广泛的图表程序类别。 特别是, 许多嵌入循环程序可以通过新的计算来验证 。

1
下载
关闭预览

相关内容

【CIKM2020】神经逻辑推理,Neural Logic Reasoning
专知会员服务
49+阅读 · 2020年8月25日
49篇ICLR2020高分「图机器学习GML」接受论文及代码
专知会员服务
61+阅读 · 2020年1月18日
【精通OpenCV 4】Mastering OpenCV 4 - Third Edition 随书代码
专知会员服务
38+阅读 · 2019年11月13日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
【新书】Python编程基础,669页pdf
专知会员服务
193+阅读 · 2019年10月10日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
39+阅读 · 2019年10月9日
MIT新书《强化学习与最优控制》
专知会员服务
275+阅读 · 2019年10月9日
图机器学习 2.2-2.4 Properties of Networks, Random Graph
图与推荐
10+阅读 · 2020年3月28日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
已删除
将门创投
5+阅读 · 2019年4月15日
强化学习的Unsupervised Meta-Learning
CreateAMind
17+阅读 · 2019年1月7日
LibRec 精选:连通知识图谱与推荐系统
LibRec智能推荐
3+阅读 · 2018年8月9日
条件GAN重大改进!cGANs with Projection Discriminator
CreateAMind
8+阅读 · 2018年2月7日
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
Adversarial Variational Bayes: Unifying VAE and GAN 代码
CreateAMind
7+阅读 · 2017年10月4日
Auto-Encoding GAN
CreateAMind
7+阅读 · 2017年8月4日
Arxiv
0+阅读 · 2021年1月22日
Arxiv
0+阅读 · 2021年1月21日
Arxiv
0+阅读 · 2021年1月19日
Arxiv
0+阅读 · 2021年1月19日
Arxiv
7+阅读 · 2019年6月20日
Logic Rules Powered Knowledge Graph Embedding
Arxiv
7+阅读 · 2019年3月9日
Embedding Logical Queries on Knowledge Graphs
Arxiv
5+阅读 · 2018年9月6日
VIP会员
相关主题
相关VIP内容
【CIKM2020】神经逻辑推理,Neural Logic Reasoning
专知会员服务
49+阅读 · 2020年8月25日
49篇ICLR2020高分「图机器学习GML」接受论文及代码
专知会员服务
61+阅读 · 2020年1月18日
【精通OpenCV 4】Mastering OpenCV 4 - Third Edition 随书代码
专知会员服务
38+阅读 · 2019年11月13日
强化学习最新教程,17页pdf
专知会员服务
174+阅读 · 2019年10月11日
【新书】Python编程基础,669页pdf
专知会员服务
193+阅读 · 2019年10月10日
【SIGGRAPH2019】TensorFlow 2.0深度学习计算机图形学应用
专知会员服务
39+阅读 · 2019年10月9日
MIT新书《强化学习与最优控制》
专知会员服务
275+阅读 · 2019年10月9日
相关资讯
图机器学习 2.2-2.4 Properties of Networks, Random Graph
图与推荐
10+阅读 · 2020年3月28日
Hierarchically Structured Meta-learning
CreateAMind
26+阅读 · 2019年5月22日
Transferring Knowledge across Learning Processes
CreateAMind
27+阅读 · 2019年5月18日
已删除
将门创投
5+阅读 · 2019年4月15日
强化学习的Unsupervised Meta-Learning
CreateAMind
17+阅读 · 2019年1月7日
LibRec 精选:连通知识图谱与推荐系统
LibRec智能推荐
3+阅读 · 2018年8月9日
条件GAN重大改进!cGANs with Projection Discriminator
CreateAMind
8+阅读 · 2018年2月7日
【论文】变分推断(Variational inference)的总结
机器学习研究会
39+阅读 · 2017年11月16日
Adversarial Variational Bayes: Unifying VAE and GAN 代码
CreateAMind
7+阅读 · 2017年10月4日
Auto-Encoding GAN
CreateAMind
7+阅读 · 2017年8月4日
相关论文
Arxiv
0+阅读 · 2021年1月22日
Arxiv
0+阅读 · 2021年1月21日
Arxiv
0+阅读 · 2021年1月19日
Arxiv
0+阅读 · 2021年1月19日
Arxiv
7+阅读 · 2019年6月20日
Logic Rules Powered Knowledge Graph Embedding
Arxiv
7+阅读 · 2019年3月9日
Embedding Logical Queries on Knowledge Graphs
Arxiv
5+阅读 · 2018年9月6日
Top
微信扫码咨询专知VIP会员