Ada Tutorial（2）SPARK Examiner + SPARK Prover

news2024/11/15 12:14:42

文章目录

  • 代码 Task1.adb
  • 代码 task3.adb
  • task4.adb

在Ada和SPARK中，SPARK_Mode是一个编译指示，它表示随后的代码将使用SPARK语言规则进行编译和分析。

在with SPARK_Mode => On的影响下，编译器会在编译过程中应用SPARK语言规则，它比Ada有更严格的要求，例如禁止某些可能导致不确定行为的构造。此外，打开SPARK_Mode还会允许一些只有在SPARK中才有的特性，例如契约（即前置条件和后置条件）。

SPARK_Mode => On 的具体影响可能会因编译器和SPARK工具的版本而略有不同，但基本上，这个编译指示都会让编译器对随后的代码应用SPARK语言规则。在上面的代码中，SPARK_Mode => On应用于整个Task4包体，这意味着这个包体的所有代码都将使用SPARK规则进行编译和分析。

package body Task4 with SPARK_Mode 表示你将要开始定义一个名为 Task4 的包体，并且这个包体会使用 SPARK 的一些规则进行编译和分析。不过这里缺少 => On 或 => Off 来显式地开启或关闭 SPARK_Mode。

SPARK_Mode => On 表示你要在这个包体中使用 SPARK 的语言规则。这通常意味着代码需要满足更严格的要求，例如避免使用可能导致不确定行为的构造。
SPARK_Mode => Off 表示你要在这个包体中使用标准 Ada 的语言规则，而不使用 SPARK 的规则。
请注意，这只是编译指示，不会改变程序的行为，而是改变编译器和工具对代码的理解和处理方式。它可以帮助你编写更安全、更可靠的代码，特别是当你使用 SPARK 的一些高级特性（例如契约）时。

代码 Task1.adb

package body Task1 with
     SPARK_Mode => On
is

   procedure Task1Procedure(Result : out Integer) is
      Ok : Boolean;
      I, J : Integer;
   begin
      if Ok then
         I := 0;
         J := 0;
      end if;

      Result := I + J;
   end Task1Procedure;

end Task1;

题目：run SPARK examiner over the source code in task1.adb by going to Spark → Examine File from the GPS menu.
This reports that the variable Ok is used without being initialised, and the variables I and J are only initialised if Ok is true. Note the difference between a variable being never initialised (Ok), and a variable possibly being uninitialised (I and J).
Note the differences between the compiler errors/warnings, and the SPARK examiner errors/warnings.
在这里插入图片描述

  • SPARK Examiner 是 SPARK 工具集中的一个组件，它负责对 SPARK 程序进行语法和语义分析，以及数据和信息流分析。

  • 语法和语义分析： SPARK Examiner 负责检查程序是否遵守 SPARK Ada 的语法和语义规则。因为 SPARK 是 Ada 的一个子集，其规则更加严格，用来保证程序的可靠性和安全性。

  • 数据和信息流分析： 这是 SPARK Examiner 的一个主要功能，它会分析数据在程序中的流动路径，以及数据之间的依赖关系。通过这个分析，Examiner 可以确保所有的数据在被读取之前已经被赋值，所有的输入都被正确地使用，没有数据竞态等问题。

通过这些分析，SPARK Examiner 可以在程序执行之前就发现许多潜在的错误和问题，从而帮助提高程序的可靠性和安全性。这些分析结果也为后续的 SPARK Prover（一个用于进行形式化证明的工具）提供了基础。

问题：Modify the source code from task 1 to include an ineffective statement, which is a statement that can be removed from a program without changing the behaviour of that program. Run the examiner over the modification, and analyse the results. Do these types of problems look familiar? (HINT: Think back to data-flow analysis in SWEN90006!)

  • 在上述的 Ada 代码中，Ok 变量被声明但从未初始化或赋值，但在程序中仍进行了 if Ok then 的判断，这其实已经是一个无效语句，因为它的行为是不确定的。 但如果我们想要明确添加一个无效语句，我们可以添加一些不会改变程序行为的代码。比如，我们可以在程序的末尾添加一个对变量 I 或 J 的赋值，如下：
package body Task1
with
     SPARK_Mode => On
is

   procedure Task1Procedure(Result : out Integer) is
      Ok : Boolean;
      I, J : Integer;
   begin
      if Ok then
         I := 0;
         J := 0;
      end if;

      Result := I + J;
      I := I;  -- 添加的无效语句
   end Task1Procedure;

end Task1;

在这里插入图片描述

代码 task3.adb

问题：Now, open and compile the source code in task3.adb, and then run the SPARK examiner and GNATProve over the file. To run GNATProve, select Spark → Prove File. Click Execute.
Why do you think the proof from task3.adb could not be proved?

package body Task3 with
     SPARK_Mode => On
is

   procedure Task3Procedure(Input : in Integer; Result : out Integer)
   is
   begin
--      if Input * 10 <= Integer'Last and
--        Input * 10 >= Integer'First then
         Result := Input * 10;
--      else
--         Result := Input;
--      end if;
   end Task3Procedure;
end Task3;

在这里插入图片描述

  • 根据提供的代码片段，这段程序可能无法通过 SPARK Prover 的证明，最可能的原因是它没有明确设定Result的范围。
  • 在这段代码中，我们的程序将输入参数Input乘以10并将结果存储在Result中。这里可能的问题是，如果Input的值过大（比如，接近整数类型的上限），那么乘以10之后可能会导致整数溢出。这样，Result就可能会包含一个无效的值，从而导致证明失败。

题目：Go to the source file task3.adb and uncomment the commented lines. Re-run the the SPARK examiner and GNATProve, and see what changes.
Is the program still not proved? If not, try to change the program to correct this problem.
HINT: Remember Integer’First Integer’Last return the lowest and highest integers respectively.
If you are struggling with this task, complete the rest of the workshop and come back to it.

package body Task3 with
     SPARK_Mode => On
is

   procedure Task3Procedure(Input : in Integer; Result : out Integer)
   is
   begin
    if Input * 10 <= Integer'Last and
      Input * 10 >= Integer'First then
         Result := Input * 10;
    else
       Result := Input;
    end if;
   end Task3Procedure;
end Task3;
  • 当我们将原本注释的部分解开之后，发现还是无法证明
    在这里插入图片描述
  • 这是因为当验证 Input * 10 的时候这个值就已经 overflow 了，因此，我们应该将代码改成下面的形式：
    在这里插入图片描述

task4.adb

-- task4.adb
package body Task4 with
SPARK_Mode => On
is
   procedure Task4Procedure(AnArray : in out MyArray; AnIndex : in Index) is
   begin
      AnArray(AnIndex) := AnArray(AnIndex) + 1;
   end Task4Procedure;
end Task4;

-- task4.ads 文件
package Task4 with
SPARK_Mode => On
is

   subtype Index is Integer range 1 .. 10;
   type MyArray is array(Index) of Integer;

   -- Returns the element of AnArray at the specified index, AnIndex.
   procedure Task4Procedure(AnArray : in out MyArray; AnIndex : in Index);
end Task4;

问题： Run the SPARK examiner and GNATProve over the code task4.adb.
The inability to prove this is actually an indication that the program is not a valid SPARK program (although this is not always the case – sometimes the tools are just not powerful enough to prove some properties). What do you think this failed proof relates to? How could you re-write this to arrive at a correct SPARK program? The relevant types are declared in task4.ads.
在这里插入图片描述

  • 在 SPARK 程序中，对于任何可能引发运行时错误的操作，都需要提供足够的前提条件来证明这种错误不会发生。 在 Task4Procedure 中，直接访问数组元素 AnArray(AnIndex) 可能会导致越界错误，如果 AnIndex 不在 AnArray 的索引范围内。

  • 同时，还要注意的是 AnArray(AnIndex) + 1 可能会导致整数溢出，如果 AnArray(AnIndex) 已经是 Integer'Last 。

  • 所以，需要提供前提条件，以证明 AnIndex 在 AnArray 的索引范围内，并且 AnArray(AnIndex) 不是 Integer'Last。在 SPARK 中，可以使用合同 (contracts) 来提供这样的前提条件。具体的修订版本如下：

-- task4.ads 文件
package Task4 with
SPARK_Mode => On
is

   subtype Index is Integer range 1 .. 10;
   type MyArray is array(Index) of Integer;

   -- Returns the element of AnArray at the specified index, AnIndex.
   procedure Task4Procedure(AnArray : in out MyArray; AnIndex : in Index) with
     Pre => (AnIndex < Integer'Last and AnArray(AnIndex) < Integer'Last);
end Task4;
  • 在 ads 文件中的 Task4Procedure 定义中通过 with 关键字加入 pre 的检查，要保证两个方面：
    • anIndex 首先没有越界风险
    • 通过 anIndex 从 AnArray 中索引出的值 AnArray(AnIndex) 没有 overflow

问题：Modify line 5 of task4.adb from:
AnArray(AnIndex) := AnArray(AnIndex) + 1;
to:
AnArray(AnIndex) := AnArray(0);
Run the SPARK examiner over note the error message. This error will also be generated by the GNAT compiler.

package body Task4 with
SPARK_Mode => On
is

   procedure Task4Procedure(AnArray : in out MyArray; AnIndex : in Index) is
   begin
      AnArray(AnIndex) := AnArray(0);
   end Task4Procedure;
end Task4;

在这里插入图片描述

  • 从 ads 文件中可以看出：subtype Index is Integer range 1 .. 10;
  • 索引 index 的范围是 1..10 因此如果是 Anarray(0) 则一定会报错
  • 同时注意这里报错是：Constraint_Error

在 Ada 中，Constraint_Error 是一种预定义的异常，通常在尝试超越数据类型的允许范围时引发。例如，如果一个整数类型的变量被限制在1到10的范围内，然后你尝试将此变量赋值为11，那么就会触发 Constraint_Error 异常。
在处理数组时，如果你尝试访问超出数组索引范围的元素，也会引发 Constraint_Error。例如，对于一个大小为10的数组，尝试访问第11个元素会导致 Constraint_Error。
此外，如果一个函数或过程的参数不满足指定的先决条件，也会引发 Constraint_Error。
处理 Constraint_Error 的常见方法是使用异常处理语句捕获并处理它。例如：

begin
   -- code that might raise a Constraint_Error
exception
   when Constraint_Error =>
      -- handle the error
end;
  • 这种处理可以使程序在遇到 Constraint_Error 时不会立即崩溃，而是可以执行错误处理代码，可能是记录错误、通知用户或尝试恢复。

题目：Modify line 5 of task4.adb from:
AnArray(AnIndex) := AnArray(AnIndex) + 1;
to:
AnArray(AnIndex) := AnArray(AnIndex + 1);
Run the SPARK examiner over this and see what has failed to prove. What do you think this failed proof relates to?

package body Task4 with
SPARK_Mode => On
is

   procedure Task4Procedure(AnArray : in out MyArray; AnIndex : in Index) is
   begin
      AnArray(AnIndex) := AnArray(AnIndex + 1);
   end Task4Procedure;
end Task4;

在这里插入图片描述

  • 这时候可能出问题的情况是：AnArray(AnIndex + 1) 中的 AnIndex + 1 可能超过 Index 的上界，因此在这里我们更改 ads 代码中的 pre 条件
package Task4 with
SPARK_Mode => On
is

   subtype Index is Integer range 1 .. 10;
   type MyArray is array(Index) of Integer;

   -- Returns the element of AnArray at the specified index, AnIndex.
   procedure Task4Procedure(AnArray : in out MyArray; AnIndex : in Index)
     with
       Pre => (AnIndex < Index'Last and AnArray(AnIndex) < Integer'Last);
end Task4;
  • 使得 AnIndex < Index'Last 这样就可以了

本文来自互联网用户投稿，该文观点仅代表作者本人，不代表本站立场。本站仅提供信息存储空间服务，不拥有所有权，不承担相关法律责任。如若转载，请注明出处：http://www.coloradmin.cn/o/638058.html

如若内容造成侵权/违法违规/事实不符，请联系多彩编程网进行投诉反馈，一经查实，立即删除！

相关文章

基于“声音”的量子计算机 | Science速递

基于“声音”的量子计算机 | Science速递

光子盒研究院 现在&#xff0c;一个基于声音的量子计算机关键构件已被首次被证明是有效的。 构建量子计算机的一种流行方式是将信息编码到光粒子的量子状态中&#xff0c;然后将它们送过镜子和透镜等“迷宫”般的设备阵列来操纵这些信息。量子力学定律指出&#xff0c;量子粒子…
阅读更多...
关于B/S结构系统的会话session机制

关于B/S结构系统的会话session机制

用户打开浏览器&#xff0c;进行一系列操作&#xff0c;然后最终将浏览器关闭&#xff0c;这整个过程叫做一次会话&#xff0c;会话对象叫session 用户在浏览器上点击了一次超链接或按钮等&#xff0c;称为一次请求&#xff0c;java对象是request session机制属于B/S结构的一部…
阅读更多...
项目 引入 uView

项目 引入 uView

只分享干货&#xff01; 第一点&#xff1a; npm install uview-ui//或yarn add uview-ui 第二点 import Vue from vue; import uView from uview-ui;Vue.use(uView);//或// main.js import uView from /node_modules/uview-ui Vue.use(uView) 第三点 import /node_module…
阅读更多...
RK3568开发板 buildroot配置文件

RK3568开发板 buildroot配置文件

在上一期技术分享中我们学会了如何在buildroot里选中我们自己想要的软件&#xff0c;如vsftpd、openssh等&#xff0c;那么有些客户可能会有疑问&#xff0c;安装完软件后需要配置相应的环境&#xff0c;应该怎么样默认的配置在系统中呢&#xff1f;其实这里的话已经为大家考虑…
阅读更多...
python kafka 指定消费者名字

python kafka 指定消费者名字

#!/usr/bin/env python # codingutf-8 """ kafka的消费者不是线程安全的&#xff0c;不能多线程启用 kafka不像其他的MQ&#xff0c;消费完数据&#xff0c;直接丢掉&#xff0c;而是会默认存储7天&#xff0c;存储7天后自动清除&#xff0c;故而可以从…
阅读更多...
AI虚拟数字人在医学领域的四大应用场景

AI虚拟数字人在医学领域的四大应用场景

AI虚拟数字人技术是一种基于计算机图形学和人工智能技术的新型应用&#xff0c;可以模拟人类的外貌、语言、行为等特征&#xff0c;实现与人类的交互。在医疗领域中&#xff0c;AI虚拟数字人技术也有着广泛的应用前景。以下是几个可能的应用场景&#xff1a; 1.医学教育 AI虚拟…
阅读更多...
java poi生成excel折线图、柱状图、饼图、动态列表

java poi生成excel折线图、柱状图、饼图、动态列表

实现效果 测试类 public class ChartTest {// 开始行public static int chartRowStart 3;// 结束行public static int chartRowEnd 20;public static ChartPosition chartPosition;public static void main(String[] args) throws IOException {// 填充数据XSSFWorkbook work…
阅读更多...
30个Python代码，10分钟get常用技巧！

30个Python代码，10分钟get常用技巧！

关注“Python专栏”&#xff0c;搜索暗号【面试大全】立即领取面试题简历模板。 学 Python 怎样才最快&#xff0c;当然是实战各种小项目&#xff0c;只有自己去想与写&#xff0c;才记得住规则。本文是 30 个极简任务&#xff0c;初学者可以尝试着自己实现&#xff1b;本文同样…
阅读更多...
DVWA-XSS (Stored)

DVWA-XSS (Stored)

跨站点脚本 &#xff08;XSS&#xff09;”攻击是一种注入问题&#xff0c;其中恶意脚本被注入到原本良性和受信任的网站上。 当攻击者使用 Web 应用程序发送恶意代码&#xff08;通常以浏览器端脚本的形式&#xff09;时&#xff0c;就会发生 XSS 攻击&#xff0c; 给其他最终…
阅读更多...
腾讯云数据库mysql报错sql_mode=only_full_group_by的解决方法

腾讯云数据库mysql报错sql_mode=only_full_group_by的解决方法

原因:mysql5.6和5.7兼容问题 解决方法: sql_mode“ONLY_FULL_GROUP_BY” 把这个去掉
阅读更多...
如何优雅的自动修改node_modules 中的依赖包内容？

如何优雅的自动修改node_modules 中的依赖包内容？

使用 patch-package 自动修改 项目中node_modules中内容 背景简介&#xff1a;我们在使用第三方依赖包时如果遇到了 bug&#xff0c;通常解决的方式都是绕过这个问题&#xff0c;使用其他方式解决&#xff0c;较为麻烦。或者给作者提个 issue 或者 PR&#xff0c;然后等待作者的…
阅读更多...
真有无限流量上网设备吗？必须是那种真无限流量、不限速的

真有无限流量上网设备吗？必须是那种真无限流量、不限速的

提到无限流量&#xff0c;七八年前确实有这种说法&#xff0c;而且是官方说法&#xff0c;三大运营商卡套餐都有无限流量这一说。比如当时电信推出过一款99元/月流量无限用的手机卡套餐&#xff0c;移动运营商出过一款89元/月的类似产品&#xff0c;都是打着无限流量的标语&…
阅读更多...
Android 13-SystemUI 屏幕左上角或者左上交显示绿色亮点，去掉该亮点

Android 13-SystemUI 屏幕左上角或者左上交显示绿色亮点，去掉该亮点

packages/SystemUI/src/com/android/systemui/privacy/PrivacyConfig.kt private const val DEFAULT_MIC_CAMERA false 改成false就好了
阅读更多...
Randoop随机测试自动生成测试用例

Randoop随机测试自动生成测试用例

什么是Randoop&#xff1a; Randoop是一个为JAVA单元测试生成测试用例的框架&#xff08;生成器&#xff09;&#xff0c;它基于Junit格式为编译后JAVA字节码&#xff08;classes&#xff09;自动生成测试用例. Randoop通过反馈式的随机测试来生成测试用例&#xff0c;由于测…
阅读更多...
工程项目管理常用的软件有哪些？

工程项目管理常用的软件有哪些？

工程项目管理常用的软件有哪些&#xff1f; 市面上的项目管理工具各种类型的都有&#xff0c;各自也有各自的优势和特点&#xff0c;但是“一千个人眼里有一千个哈姆雷特”&#xff0c;A企业觉得好用的项目管理工具不一定适合B企业。 一般来说&#xff0c;企业在进行系统工具…
阅读更多...
蚁群优化算法

蚁群优化算法

目录 蚁群优化 Quadratic Assignment Problem (QAP) 主要代码 create model Cost RouletteWheelSelection Plot 结果 蚁群优化 蚁群优化&#xff08;ACO&#xff09;是一套概率元启发法和智能优化算法&#xff0c;其灵感来源于蚂蚁的社会行为。ACO算法也被归类为群集智能…
阅读更多...
电脑系统可以直接备份到其它硬盘上吗

电脑系统可以直接备份到其它硬盘上吗

在日常使用电脑的过程中&#xff0c;我们都希望能够保护好重要的系统数据&#xff0c;以防止意外数据丢失或系统崩溃。那么&#xff0c;能否将电脑系统直接备份到其他硬盘上呢&#xff1f;本文将为您解答这个问题&#xff0c;并探讨备份系统的方法和注意事项。 工具/原料&…
阅读更多...
Kubernetes通过滚动更新deployment实现金丝雀发布

Kubernetes通过滚动更新deployment实现金丝雀发布

如果要使用 Deployment 向用户子集或服务器子集上线版本&#xff0c; 则可以遵循资源管理所描述的金丝雀模式&#xff0c; 创建多个 Deployment&#xff0c;每个版本一个。 所谓金丝雀发布&#xff08;Canary Release&#xff09;&#xff0c;就是第一个新的 Pod 创建完成后立…
阅读更多...
高考落榜，误打误撞学习了软件测试现在月薪30k成为了班上人人羡慕的对象

高考落榜，误打误撞学习了软件测试现在月薪30k成为了班上人人羡慕的对象

记得我刚高考结束时&#xff0c;并没有想象中的狂欢&#xff0c;反而是一种处于一种坐立不安的焦虑中&#xff0c;因为那时单纯地认为&#xff1a;这张试卷&#xff0c;将决定我的一生。对于将信仰寄托于高考的学生来说&#xff0c;当网页上高考成绩弹出的一瞬间&#xff0c;世…
阅读更多...
数据在内存中的存储--浮点数

数据在内存中的存储--浮点数

那么好了好了&#xff0c;宝子们&#xff0c;今天给大家介绍一下 “数据在内存中储存” 的来龙去脉---浮点数&#xff0c;来吧&#xff0c;开始整活&#xff01;⛳️ 一、数据类型家族&#xff08;浮点数&#xff09; 家族成员&#xff1a;float&#xff0c;double&#xf…
阅读更多...
推荐文章
最新文章

Copyright @ 2022~2023