问题标签 [formalize]
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.
compass-sass - 中间人，指南针和形式化
我一直试图让中间人、指南针和正式化一起工作，但到目前为止还没有太多运气。
我确实安装了 Compass Formalize 插件
...我确实添加了强制性要求config.rb
...但效果是我的样式表可以定位（使用@import "formalize";
），但我不知道如何提取 JavaScript 文件。任何人？
css - ie/chrome 中的formalize.css 按钮
我在设置按钮样式时遇到了一些问题。
我正在使用来自http://formalize.me/的formalize.css 和 Eric Meyer CSS Reset。
这是在 IE 和 Chrome 中发生的情况：
按钮的类如下所示：
关于为什么描述似乎超出了 IE 和 Chrome 中的正常位置的任何建议？
uml - 如何形式化 Uml
有没有办法将 UML 转换（形式化）为 Z 表示法？我的意思是有什么方法可以将 UML 需求重写为像 z 这样的正式语言？
对不起我的英语不好，我的母语不是英语。谢谢你。
operating-system - 事件 B 证明义务
我在事件 B 中遇到了解除证明义务的问题。在我的工作中，我想将内存保护要求的规范形式化，以检查它们之间的一致性。为此，我使用 Event-B Context 来形式化系统的结构，并使用 Event-B Machine 来描述需求。每个需求都在 Invariant 和 Event 中进行了描述。Event-B 将检查每对需求以发现不一致之处。
但是，它不能证明两个要求是一致的： 1：“ NonTrusted对其他 OS_App的data_section 的读取访问权限是may_prevent ”
2：“来自OS_App的读写访问权限
对其自己的 data_section是shall_permit "
这是我的工作。首先，在上下文文件中，我描述了系统的结构和访问控制：
1. 系统的结构：
我们有两种类型的 OS_Application：Trusted和NonTrusted。
2 种 OS_Objects：Tasks和ISRs。
2 种 ISR：Category_1和Category_2。
每个 OS_Object 属于一个 OS_App：ContainerOf ∈ OS_Obj → OS_App
每个 OS_App 都有一个代码段：AppCode ∈ OS_App → CodeSection
内存有 2 个部分：DataSection和Stack
OS_App 和 OS_Obj可能有 DataSection：
- AppData ∈ OS_App ⇸ DataSecs
- ObjData ∈ OS_Obj ⇸ DataSecs
OS_Obj 有自己的 Stack：ObjStack ∈ OS_Obj → Stacks
2.访问控制：
访问是从Subjects到Objects：
Subjects包括：OS_App和OS_Obj
Objects包括：Code_Section和Memory
在下面的代码中，第20行描述：“这些对象的堆栈，根据定义，只属于所有者对象，因此不需要在对象之间共享堆栈数据，即使这些对象属于同一个操作系统应用程序。”
第 21 行描述：“代码部分是 OS 应用程序私有的，或者可以在所有 OS 应用程序之间共享”
第 22、23 行描述：“OS 应用程序可以有私有数据部分，而任务/ISR 可以有私有数据部分。 "
第 24 行描述：“操作系统应用程序的私有数据部分属于该操作系统应用程序的所有任务/ISR 共享。”
通过分析，我将上下文定义如下：
其次，在机器文件中，我描述了：
以及两个事件：两个事件
之后，事件-B 生成 Proof Obligations 并尝试证明一致性。但是，这两个要求是不一致的，如下：
undischarged Proof Obligation
In the Goal box：它不能证明：
A = (¬(app∈dom(AppData) ∧ app1=app ∧ AppData(app2)=AppData(app)))是真的。
但是，在要求 2 中，我们有：app1 ≠ app2
=> app ≠ app2 (because app1=app)
=>AppData(app2) ≠ AppData(app)
因此，(app∈dom(AppData) ∧ app1=app ∧ AppData(app2)=AppData(app)= FALSE
然后 A = (¬(app∈dom(AppData) ∧ app1=app ∧ AppData(app2)=AppData(app)))= TRUE。
请给我一些提示或评论好吗？
distributed-system - 关于 TLA+ 中的常量运算符的问题
我最近正在阅读“指定系统”一书。在第 5 章中，Leslie 定义了常量运算符 Send( , , , )。
我对如何为这个常量表达式赋值（真/假）感到困惑？我们是否需要为 TLC 模型检查器中的每个 (p, v, m, m') 分配真/假？