问题标签 [z-notation]

For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.

0 投票
1 回答
61 浏览

isabelle - Isabelle/HOL 与 HOL-Z 和 ZETA

我看过一些论文,描述了如何使用工具 HOL-Z 和 ZETA 将 Z 表示法与 Isabelle/HOL 一起使用。我找不到这些工具,它们曾经发布过吗?还有其他方法可以将 Isabelle 与 Z 表示法一起使用吗?

0 投票
0 回答
15 浏览

formal-languages - 如何在 Z 规范中查找日期差异

我有下面定义的日期模式

以及下面定义的捐赠日期检查模式

我想检查最后一次捐款是否已经过去了三个月 我如何检查差异?

我减去了日期并假设他们给出了这些天之间的天数但我不确定实际的解决方案

0 投票
0 回答
16 浏览

linked-list - Write a linked list operational schemas in Z language in latex

I am trying to write all operational schemas of Linked List in Z specification using latex. I have written the following schemas of linked list in latex software. Please check that I have created right schemas or wrong. If wrong please correct. Here is the code of schemas for linked list in Latex.

0 投票
0 回答
3 浏览

typechecking - 安装法兹。错误:exp '=', ',', ';', 'asm' or '__attribute__' before 'x_slot'ected

我正在 Ubuntu 20.04 https://spivey.oriel.ox.ac.uk/corner/Fuzz_typechecker_for_Z中安装“Fuzz typechecker Z”

但是,当我这样做时,make会出现以下错误。知道我应该从哪里开始吗?

我知道这可能是一个与 Fuzz 相关的非常具体的问题,因此感谢您的帮助。以下是文件列表(zparse.c、zparse.h、absyn.h) https://github.com/Spivoxity/fuzz/tree/master/src