问题标签 [spark-ada]
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.
ada - 在下面的 ADA Spark 示例中，我如何阻止先决条件失败
对于一个项目，我目前正在尝试为想象中的飞机编写一个小型飞行员辅助系统。任务是学习 Ada Spark，而不是航空电子设备。我已经对我希望使用的飞机组件进行了建模，在主文件中进行了一些测试以检查组件是否按预期工作，一切都很好，现在我要在函数中添加前置条件和后置条件以确保我的飞机是超级的安全的。一种这样的安全措施是确保在飞机被拖曳时不能打开发动机，反之亦然，在发动机打开时切换到拖曳。
我将引擎建模为高度复杂的记录，具有一个属性，类型 OnOff，它采用值 On 或 Off 之一。注意我计划扩展属性，所以它不会保留一个属性记录。
这是引擎规范文件
我的飞机是这样组装的：
planes 文件中的过程 switchOnEngine 将引擎作为输入，并从引擎文件中调用 switchOn。这是规格，下面是正文：
飞机作为变量传入，因此我可以检查我的前后条件的各种属性，但我收到警告消息，我不确定如何解决。
以下行也从我控制我的飞机的主文件中给出错误
这是主文件中飞机的初始化
任何帮助都会很棒。我认为在飞机不能被拖曳的前提下建议就足够了，但似乎还不够。
ada - Ada GNAT 证明 1 不 >= 0
我试图证明，我在数组中查找第二大值的算法可以正常工作。这是我的代码：
这是我的前置条件和后置条件：
我现在被 GNATprove 的这条消息卡住了：
如果我没记错的话，它指的是关于结果大于或等于 0 的第一个条件，那么为什么将 1 作为反例呢？有什么办法可以证明这一点吗？
ada - 前置条件和后置条件是否取代了函数验证？
我一直在尝试学习使用 SPARK 的基础知识，并且我已经使用前置和后置条件进行了研究，但我不确定它们是否可以代替验证？例如，除非所有门都关闭并锁定，否则飞机不会切换到起飞模式的功能。我是否需要在程序主体中添加代码来停止这种行为，或者前置条件和后置条件是否足够？我不清楚，因为我的课程教程实际上都没有这样做，但是当我测试程序时，我不受违反条件的限制。
ada - 如何在 Spark_Ada 中检查 Storage_Error
根据 Spark2014 文档，不允许在 Spark 代码中处理异常。
通过验证，可以排除大多数运行时错误发生在编写的程序内部，但Storage_Error不能排除诸如此类的异常。
由于Storage_Error可能发生在每个过程/函数调用或使用动态分配内存时new（如果我错了，请纠正我），因此在 Spark_Mode=off 的代码段中捕获和处理此异常仅在最高级别有效程序（程序的入口点）。我真的不喜欢这种方法，因为您几乎失去了对这种异常做出反应的所有可能性。
我想做的事：
假设用一个过程创建一个无界树Add()。在这个过程中，我想检查堆上是否有足够的空间，以便在树内创建一个新节点。如果有，为节点分配内存并将其添加到树中，否则可以给出一个 out 参数，其中设置了某种标志。
我已经通过 Spark UserGuide 进行了搜索，但无法找到一种应该如何处理的方法，只是程序员必须确保有足够的可用内存，而不是如何做到这一点。
如何在 Spark 中处理这些异常？
ada - 对于可能在函数或过程中释放的访问类型，如何处理 **Post** 合约中的“旧”属性？
假设具有以下设置：
注意：上面的代码可能并不完全有效，但我希望这个概念是可以理解的。
现在如果Unchecked_Deallocation()在Self内部使用Replace
并且分配了一个新的 Integer 并将其设置为Self（这应该导致 Self'Old 指向一个现在无效的内存位置）会发生什么？
Ada 是否保留了Self'Old指向前一个内存位置但在Unchecked_Deallocation()执行之前的快照？
如果Self'Old在 Post 合同中使用无效，你怎么还能访问以前的值？是否可以在 Pre 合约中创建手动快照，然后可以在 Post 中使用？也许可以使用 Ghost_Code 来实现？
我想在 Spark 中制作所有东西，以防万一发生变化。
编辑：固定Self为in out西蒙赖特提到的。
编辑：Self允许的固定类型null
ada - 如何访问具有该过程作为访问参数的过程/函数的 Pre/Post 合同中的过程参数？
Containers.Vector包定义了一些可以作为参数访问过程的过程。此过程支持一个参数。
例子：
是否可以在程序的E前后合同中使用？Query_ElementUpdate_Element
写类似：
导致编译错误："E" is undefined
如果可能，该解决方案应该与 Spark 兼容。
ada - （SPARK Ada）作为数字类型元素在 0-9 范围内给出的数字？
我正在尝试在 SPARK Ada 中创建一个递减程序。D1 到 D3 是用户输入的输入数字，程序要求将 3 位数字减 1 并输出 3 位数字 O1、O2、O3。我不确定如何将其修改为数字类型的元素。然后我将对其进行调整，以便将数字作为由 3 位数字组成的记录类型给出。对有用的网站/解释的任何帮助将不胜感激。
Eg1 of program) if d1=1 d2=2 d3=3 then output = 122. Eg2 of program) input d1=0 d2=0 d3=0 then output = 999.
到目前为止，这是我的源代码：