Ada Tutorial（2）SPARK Examiner + SPARK Prover

文章目录

  • 代码 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.mfbz.cn/a/28077.html

如若内容造成侵权/违法违规/事实不符，请联系我们进行投诉反馈qq邮箱809451989@qq.com，一经查实，立即删除！

相关文章

C语言之数组详解（1）（更新前面数组博客的不足）

C语言之数组详解（1）（更新前面数组博客的不足）

目录 一、一维数组 1.一维数组的创建和初始化 (1).数组的创建 (2).数组的初始化 2.一维数组的使用 3.一维数组在内存中的存储 二、二维数组 1.二维数组的创建和初始化 (1).二维数组的创建 (2).二维数组的初始化 2.二维数组的使用 3.二维数组在内存中的存储 三、数组作为函数参…
阅读更多...
微软发布自己的 Linux 发行版：Azure Linux

微软发布自己的 Linux 发行版：Azure Linux

导读在内部使用两年并自 2022 年 10 月起以公共预览版运行后&#xff0c;微软终于在日前正式公开发布了其 Azure Linux 的发行版。 在内部使用两年并自 2022 年 10 月起以公共预览版运行后&#xff0c;微软终于在日前正式公开发布了其 Azure Linux 的发行版。 微软 Azure Lin…
阅读更多...
DSDP140B 57160001-ACX

DSDP140B 57160001-ACX

​ DSDP140B 57160001-ACX DSDP140B 57160001-ACX 单相漏电保护器可以接在三相四线制电路中使用 单相漏电维护器不可以接在三相四线制电路中使用。术有专攻&#xff0c;单相漏电开关在漏电维护器内部装置的零序电流互感器检测的是一根相线&#xff08;前方&#xff09;和一…
阅读更多...
完型填空技巧

完型填空技巧

完形中分值最高的是逻辑关系题&#xff0c;逻辑关系分为两种&#xff0c;一种是选项就是逻辑关系的&#xff0c;例: Given the advantages of electronic money, you might thinkthat we would move quickly to the cashless society in which allpayments are made electronic…
阅读更多...
【C++】红黑树的模拟实现

【C++】红黑树的模拟实现

文章目录 一、红黑树的概念二、红黑树的性质三、红黑树节点的定义四、红黑树结构五、红黑树的插入操作六、红黑树的调整1.叔叔存在且为红2.叔叔不存在或者存在且为黑3.插入完整代码4.总结 七、红黑树的验证八、红黑树的删除九、红黑树与AVL树的比较十、红黑树的应用十一、红黑树…
阅读更多...
LVS+Keepalived 高可用群集实战部署

LVS+Keepalived 高可用群集实战部署

LVSKeepalived 高可用群集实战部署 一、LVSKeepalived 高可用群集1.LVS2、Keepalived工作原理和作用3、Keepalived体系主要模块及其作用4、Keepalived实现原理剖析5、VRRP &#xff08;虚拟路由冗余协议&#xff09; LVSKeepalived 高可用群集部署&#xff08;抢占模式&#xf…
阅读更多...
[nlp] OPT与GPT-2的差异

[nlp] OPT与GPT-2的差异

Meta AI 开源1750亿参数大模型- OPT，FlagAI一键调用！ - 知乎简介Meta AI 开源 OPT系列模型，其中最大模型1750 亿参数（需申请访问权限）媲美 GPT-3。OPT系列模型包括了多组不同参数规模的模型权重，如图： OPT开源了一系列大模型，但是实际调用这些模型有很高的技术门槛。为…
阅读更多...
PortSwigger web缓存中毒（Cache Poisoning）

PortSwigger web缓存中毒（Cache Poisoning）

一、什么web缓存中毒&#xff1f; Web缓存中毒&#xff08;Web Cache Poisoning&#xff09;是一种攻击技术&#xff0c;攻击者通过操纵Web应用程序的缓存系统&#xff0c;将恶意或欺骗性内容注入到合法的缓存中&#xff0c;以欺骗用户或绕过安全控制。 Web缓存中毒的原理是利用…
阅读更多...
scala

scala

面向对象 Scala 的面向对象思想和Java 的面向对象思想和概念是一致的。 Scala 中语法和 Java 不同&#xff0c;补充了更多的功能。 6.1类和对象详解 6.1.1组成结构 构造函数: 在创建对象的时候给属性赋值 成员变量: 成员方法(函数) 局部变量 代码块 6.1.2构造器 每个…
阅读更多...
【宝塔建站】Ubuntu下使用宝塔面板一键搭建Z-Blog个人博客

【宝塔建站】Ubuntu下使用宝塔面板一键搭建Z-Blog个人博客

文章目录 1.前言2.网站搭建2.1. 网页下载和安装2.2.网页测试2.3.cpolar的安装和注册 3.本地网页发布3.1.Cpolar临时数据隧道3.2.Cpolar稳定隧道&#xff08;云端设置&#xff09;3.3.Cpolar稳定隧道&#xff08;本地设置&#xff09; 4.公网访问测试5.结语 1.前言 Ubuntu系统作…
阅读更多...
【深度学习】pytorch pth模型转为onnx模型后出现冗余节点“identity”，onnx模型的冗余节点“identity”

【深度学习】pytorch pth模型转为onnx模型后出现冗余节点“identity”，onnx模型的冗余节点“identity”

情況描述 onnx模型的冗余节点“identity”如下图。 解决方式 首先&#xff0c;确保您已经安装了onnx-simplifier库&#xff1a; pip install onnx-simplifier然后&#xff0c;您可以按照以下方式使用onnx-simplifier库&#xff1a; import onnx from onnxsim import simp…
阅读更多...
STM32F407软件模拟I2C实现MPU6050通讯（CUBEIDE）

STM32F407软件模拟I2C实现MPU6050通讯（CUBEIDE）

STM32F407软件模拟I2C实现MPU6050通讯&#xff08;CUBEIDE&#xff09; 文章目录 STM32F407软件模拟I2C实现MPU6050通讯&#xff08;CUBEIDE&#xff09;模拟I2C读写的实现mpu6050_iic.cmpu6050_iic.h代码分析 复位&#xff0c;读取温度&#xff0c;角度等函数封装mpu6050.cmpu…
阅读更多...
QT学习07：五种按钮控件

QT学习07：五种按钮控件

文章首发于我的个人博客&#xff1a;欢迎大佬们来逛逛 文章目录 抽象类&#xff1a;QAbstractButtonQPushButtonQToolButtonQCommandLinkButtonQRadioButtonQCheckBoxQButtonGroup 抽象类&#xff1a;QAbstractButton 是所有按钮类的祖先。 QAbstractButton的信号&#xff1a…
阅读更多...
深入理解CSS字符转义行为

深入理解CSS字符转义行为

深入理解CSS字符转义行为 深入理解CSS字符转义行为 前言为什么要转义&#xff1f;CSS 转义什么是合法css的表达式 左半部分右半部分 练习参考链接 前言 在日常的开发中&#xff0c;我们经常写css。比如常见的按钮: <button class"btn"></button>&am…
阅读更多...
【MySQL】 IS NOT NULL 和 != NULL 的区别？

【MySQL】 IS NOT NULL 和 != NULL 的区别？

背景 最近在开发小伙伴的需求&#xff0c;遇到了一个数据库统计的问题&#xff0c; is not null 结果正确 &#xff01;null 结果就不对&#xff0c;然后就激发了获取真理的想法&#xff0c;那必须的查查 咋回事嘞&#xff1f; 开整 在用MySQL的过程中&#xff0c;你是否存…
阅读更多...
大学物理（上）-期末知识点结合习题复习（4）——质点运动学-动能定理 力做功 保守力与非保守力 势能 机械能守恒定律 完全弹性碰撞

大学物理（上）-期末知识点结合习题复习（4）——质点运动学-动能定理 力做功 保守力与非保守力 势能 机械能守恒定律 完全弹性碰撞

目录 1.力做功 恒力作用下的功 变力的功 2.动能定理 3.保守力与非保守力 4.势能 引力的功与弹力的功 引力势能与弹性势能 5.保守力做功与势能的关系 6.机械能守恒定律 7.完全弹性碰撞 题1 题目描述 题解 题2 题目描述 题解 1.力做功 物体在力作用下移动做功…
阅读更多...
AWS CodeWhisperer 简单介绍

AWS CodeWhisperer 简单介绍

一、何为AWS CodeWhisperer Amazon CodeWhisperer能够理解以自然语言&#xff08;英语&#xff09;编写的注释&#xff0c;并能实时生成多条代码建议&#xff0c; 以此提高开发人员生产力。 二、主要功能 Amazon CodeWhisperer 的主要功能&#xff0c;包括代码生成、引用追踪…
阅读更多...
36.SpringBoot实用篇—运维

36.SpringBoot实用篇—运维

目录 一、实用篇—运维。 &#xff08;1&#xff09;程序打包与运行&#xff08;Windows版&#xff09;。 &#xff08;2&#xff09;spring-boot-maven-plugin插件作用。 &#xff08;3&#xff09;程序打包与运行&#xff08;Linux版&#xff09;。 &#xff08;4&#…
阅读更多...
chatgpt赋能python：Python中如何处理多个输入

chatgpt赋能python：Python中如何处理多个输入

Python中如何处理多个输入 在编写Python程序时&#xff0c;我们经常需要从用户那里获取多个输入来执行某些操作。本文将介绍Python中的各种方法来处理多个输入。 从终端获取多个输入 Python中最简单的方式是从终端获取多个输入。下面是一个基本的例子&#xff1a; input_st…
阅读更多...
SpringSecurity实现前后端分离登录token认证详解

SpringSecurity实现前后端分离登录token认证详解

目录 1. SpringSecurity概述 1.1 权限框架 1.1.1 Apache Shiro 1.1.2 SpringSecurity 1.1.3 权限框架的选择 1.2 授权和认证 1.3 SpringSecurity的功能 2.SpringSecurity 实战 2.1 引入SpringSecurity 2.2 认证 2.2.1 登录校验流程 2.2.2 SpringSecurity完整流程 2.2.…
阅读更多...
最新文章

Copyright @ 2022~2023

友情链接： 我的编程经验分享 一条长河网 尧图网站开发 尧图建网站