高完整性系统:INTRODUCING ADA

news2024/9/30 9:31:13

目录

1. ADA的历史

2. ADA的特点

2.1 Strong, Static Typing 强语言、强静态类型语言

2.1.1 ADA is Strong, Static Typing

2.1.2 C is Weak, Static Typing 

2.2 Module System

2.3 Portable

2.3.1 ADA

2.3.2 C

2.3.3 Cost of Runtime Checking

2.4 Readability 

2.4.1 Purposeful Verbosity

2.4.2 Intended Redundancy

2.4.3 Unambiguous Semantics

2.4.4 Ada Prefers Readability

2.5 Semantics and Safety 语义和安全性

2.6 Application Areas 应用领域

2.7 与MISRA C的比较

3. ADA: SOME INTERESTING HIGHLIGHTS

3.1 Packages

3.1.1 Packages: with and use

3.2 Types

3.2.1 Type Casts and Errors 

3.2.2 Subtypes

3.3 Arrays

3.4 Procedures and Functions

3.5 Parameter Passing

3.6 Parameter Modes

3.7 Implementation Hiding

3.8 Enumerations 枚举

3.9 标准类型的选择


1. ADA的历史

mid 1970s:

US DoD has too many languages for myriad embedded devices; want: safe, modular, cross platform, high level

美国国防部有太多的语言用于众多的嵌入式设备;希望:安全、模块化、跨平台、高水平

1977:

solicit proposals for new language 

征求对新语言的建议

1979:

Honeywell’s proposal chosen; christened Ada

Honeywell的提案被选中;被命名为 "Ada"。

10 Dec 1980:

MIL-STD-1815 approved

1983:

ANSI/MIL-STD-1815A (“Ada 83”)

1995:

ISO-8652:1995 (“Ada 95”) USAF funds GNAT Compiler, now in GCC

2012:

ISO/IEC 8652:2012 (“Ada 2012”)

2. ADA的特点

2.1 Strong, Static Typing 强语言、强静态类型语言

静态类型语言 VS 动态类型语言

在静态类型语言中,变量的类型必须先声明,即在创建的那一刻就已经确定好变量的类型,而后的使用中,你只能将这一指定类型的数据赋值给变量。如果强行将其他不相干类型的数据赋值给它,就会引发错误。例如C。类型检查是在编译器编译时执行的!

在动态类型语言中,没有像静态类型语言那样的限制,而是你将什么类型的数据赋值给变量,这个变量就是什么类型。如Python,JavaScript。类型检查是在编译器运行时检查的!

 强类型 VS 弱类型

强弱之分,体现在对类型的检查严格程度上,弱类型语言对于变量类型的检查比较宽松,容忍隐式类型转换这种事情的发生。何为隐式类型转换,一般有两种形式:

  1. 相关类型之间隐式转换
  2. 不相关类型之隐式间转换

举例子来说,一个int类型的数据与一个float类型的数据相加,最终的结果是一个float类型的数据,这个过程就发生了隐式类型转换,int类型数据首先被转成float类型,然后与另一个float进行操作,这便是相相关类型之间隐式转换。

一个int类型数据与一个字符串类型数据相加,竟然没有发生错误,得到的结果是一个字符串,int类型数据隐式转换为字符串,可他们原本是两个不相干的数据类型,这种就是第二种隐式转换。

在弱类型语言中,变量可以隐式强制转换为不相关类型,而在强类型语言中则不可以。

2.1.1 ADA is Strong, Static Typing

 

2.1.2 C is Weak, Static Typing 

 

2.2 Module System

Automatic dependency resolution 自动解决依赖关系

Information Hiding, Encapsulation 信息隐藏、封装

2.3 Portable

对于一个signed integer type,如果执行的操作因为它超出了该类型的基本范围,而不能提供正确的结果,就会引发异常Constraint_Error。

2.3.1 ADA

2.3.2 C

2.3.3 Cost of Runtime Checking

But stronger static checking can improve performance too.

2.4 Readability 

2.4.1 Purposeful Verbosity

这指的是一种编程语言的设计特性,其中为了确保代码清晰明了,通常需要编写更多的代码。这种语言通常比较详细,需要明确指定许多细节,而不是依赖默认行为或简洁的语法。这样的设计可以提高代码的可读性和可维护性。例如,在Ada语言中,这种特性比较明显。

2.4.2 Intended Redundancy

这是指编程语言设计时故意引入的冗余元素,以提高代码的可读性、可理解性或错误检测能力。这种冗余可能表现为需要多次指定同一信息,或者需要对相同的概念提供多种描述。例如,Ada语言强调类型的明确性和可读性,会出现这种冗余。

2.4.3 Unambiguous Semantics

这是指编程语言的语义设计得非常明确,没有或极少有模棱两可的地方。这样的设计可以使得程序的行为更加预测和一致,有助于减少由于误解语言特性而引入的错误。这是Ada和C语言等许多编程语言的共有特性。 

2.4.4 Ada Prefers Readability

Ada更偏向于代码的可读性:Ada是一种设计上注重明确性和可读性的编程语言。Ada的设计原则之一就是使得阅读程序比编写程序更容易。

为什么重视代码的可读性:一段代码可能会被阅读超过10次,但只被编写一次。因此,优化对整体成本贡献最大的任务是有意义的,也就是优化代码的可读性。这也包括了阅读你的代码的程序,如编译器和其他工具。

Ada与其他编程语言的对比:相比之下,Ruby、JavaScript、Perl这些语言更注重的是代码编写的便捷性和简洁性,而不是可读性。这种差异在语言的语义设计上有所体现。例如,JavaScript中,有些相等性比较会产生直觉上难以理解的结果,这是由于JavaScript的类型转换规则引起的。以下是一些JavaScript的例子:

JavaScript:
>>> false == 'false';
false
>>> false == '0';
true
>>> '' == '0';
false
>>> 0 == '';
true
>>> 0 == '0';
true

这些JavaScript的例子展示了一些让人困惑的语义设计,这种设计可能会影响代码的可读性和可理解性。与之相比,Ada语言会更倾向于避免此类问题,提高代码的可读性和明确性。

  • false == 'false'; 在JavaScript中,这返回false。虽然字符串'false'在逻辑上代表假,但JavaScript不会自动将字符串'false'转换为布尔值false

  • false == '0'; 这返回true。在JavaScript中,false会被转换为数字0,字符串'0'也会被转换为数字0,所以二者相等。

  • '' == '0'; 这返回false。空字符串''会被转换为0,但是字符串'0'被转换为数字时是1,所以二者不相等。

  • 0 == ''; 这返回true。空字符串''和数字0在JavaScript中被认为是相等的。

  • 0 == '0'; 这返回true。因为字符串'0'在进行比较时会被转换为数字0。

2.5 Semantics and Safety 语义和安全性

  • 运行时检查:Ada语言支持运行时检查,这包括有符号整数溢出、数组索引越界、访问未分配的内存、范围错误等。这种设计可以将难以追踪的bug(称为heisenbugs)转化为崩溃,从而更容易进行错误定位。

  • 对实时嵌入式和关键系统的安全性的影响:这些运行时检查的设计有助于提高实时嵌入式和关键系统的安全性。在这些系统中,一旦出现错误,可能会导致严重的后果。因此,能够早期检测并处理错误是非常重要的。

2.6 Application Areas 应用领域

Ada语言主要应用于实时嵌入式系统领域,这包括 Avionics 航空电子设备、Railway 铁路、Defence 国防、Space 太空、Robotics 机器人、Crypto 加密技术等。此外,Ada也应用于Muen验证分离内核,这是一种通过SPARK进行形式验证的系统。SPARK是Ada的一个子集,专注于安全和可靠性,能够支持形式化的程序验证。

2.7 与MISRA C的比较

MISRA C是一种用于汽车领域的“安全”C语言子集,但并非所有规则都是可强制执行的。相比之下,Ada本身就比C更“安全”,有更好的封装性。而SPARK则是一个比Ada更“安全”的子集,具有相同的运行时语义。

Ada拥有更强的类型系统,可以提供更多的静态保证。同时,Ada也提供了更多的运行时检查,例如数组索引越界、动态内存访问等。

因此,相比于C语言(包括其安全子集MISRA C),Ada语言(以及其子集SPARK)在设计上更注重安全性和可靠性,更适合应用于需要高度安全保障的领域。

3. ADA: SOME INTERESTING HIGHLIGHTS

3.1 Packages

Spec the interface the implementation says “what”

says "how' the implementation Body

3.1.1 Packages: with and use

3.2 Types

Type equality is by name

这段Ada代码尝试将SecondType类型的变量J赋值给FirstType类型的变量I。虽然两种类型的范围都是0到10,但在Ada语言中,这两种类型被视为不同的类型。即使它们的范围相同,它们也不能直接相互赋值。

Ada是一种静态、强类型的编程语言,这意味着你不能将一个类型的值直接赋给另一个类型的变量,除非这两个类型是相同的,或者已经定义了从一个类型到另一个类型的转换。

在这段代码中,如果你想将J赋值给I,你需要进行显式的类型转换,如下所示:

I := FirstType(J);

以上代码将J显式地转换为FirstType类型。需要注意的是,显式的类型转换可能会有潜在的风险,例如,如果J的值不在FirstType的范围内,这将会在运行时引发异常。但在这个特定的例子中,由于FirstTypeSecondType的范围是相同的,所以这种情况不会发生。

3.2.1 Type Casts and Errors 

 

这段Ada代码中的关键问题是在类型转换时可能会出现错误。这个问题的来源是BigTypeLittleType类型的范围不同。

在这段代码中,BigType类型的变量I从用户那里获取一个整数输入,然后尝试将它转换为LittleType类型并赋值给J

问题是,如果用户输入的值在BigType的范围(0..20)内,但超出了LittleType的范围(0..10),那么在类型转换时就会引发运行时异常。例如,如果用户输入了15,这个值对于BigType类型是有效的,但对于LittleType类型是无效的。

3.2.2 Subtypes

This compiles and executes with no errors.

Casting is effectively implicit between subtypes. 

 

3.3 Arrays

3.4 Procedures and Functions

Nesting, static scope

Functions with side-effects (disallowed in SPARK)

3.5 Parameter Passing

names come from names of formal parameters (which is why they must match between package spec and body) 名称来自于正式参数的名称(这就是为什么它们必须在包的规格和主体之间匹配)。

3.6 Parameter Modes

in: read only

out: write only

in out: read/write

Checked statically by the type system 

由类型系统静态检查

Allows e.g. all records to be passed by pointer if the compiler desires.

如果编译器需要,允许所有记录通过指针传递。

Note: Strong typing improving performance over e.g. C

3.7 Implementation Hiding

Vector’s fields can’t be accessed outside the package. Vector的字段不能在包之外被访问。

Why does the Vector record need to be defined in the spec?

在Ada中,有一个关键的设计原则是信息隐藏或者封装。这就意味着实现细节(比如变量的实际数据类型)应当尽可能地隐藏在包(package)的内部,而用户只能通过接口(也就是包的spec部分)来使用这个包。

在这个例子中,Vector类型在规格(spec)部分被声明为私有(private),这意味着包的使用者不能直接访问其内部结构,例如他们不能直接操作Vector中的XYZ字段。相反,他们必须通过在规格部分公开的过程(SetPrintNormalise)来操作Vector。这种设计提供了良好的封装性,有助于保护数据的完整性和一致性。

然而,Vector类型的实际定义(即其为一个包含XYZ的记录类型)需要在包的私有部分进行。这是因为包的实现部分需要知道Vector的具体结构来实现SetPrintNormalise过程。但是,尽管Vector类型在私有部分被定义,包的使用者依然不能直接访问其内部结构。

这里的两个问题实际上是相同的,都在询问为什么Vector记录需要在规格(spec)中被定义。答案是,Vector的定义实际上是在私有部分进行的,这种设计可以提供良好的封装性,防止数据的误操作。同时,这也是Ada语言的设计原则之一,即尽可能地隐藏实现细节,而只通过接口暴露出必要的操作和功能。

虽然Ada语言在设计上强调了信息隐藏和封装,但在编译阶段,编译器仍然需要知道数据类型的大小,以便为变量分配合适的内存空间。这是为什么在Ada的包规格(spec)部分,需要对Vector类型进行私有(private)声明。

在这个例子中,当编译VectorTest程序时,编译器需要知道Vector类型的大小,以便为变量V分配足够的内存空间。尽管Vector的具体定义是在包的私有部分,但由于Vector在规格部分被声明为私有类型,编译器可以根据私有部分的定义来确定其大小。

这种设计在保证封装性的同时,也确保了编译器可以正确地为类型分配内存。这是一种在保护数据完整性和一致性的同时,确保代码可执行和高效的方法。

3.8 Enumerations 枚举

枚举是一种包含有限个元素的数据类型。在Ada语言中,你可以通过列举所有可能的值来定义枚举类型。例如,以下代码定义了一个Day枚举,包含了一周的七天:

type Day is (Monday, Tuesday, Wednesday, Thursday, Friday, Saturday, Sunday);

Ada还提供了一些内置的属性,可以用于访问枚举类型的第一个元素('First)和最后一个元素('Last),以及所有可能的元素范围('Range)。

你也可以使用枚举类型作为数组的索引类型,如下所示:

Temperatures : array (Day) of Float;

上述代码定义了一个名为Temperatures的数组,其索引类型为Day,元素类型为Float。你可以使用枚举类型的元素来访问和修改数组的元素。

Ada支持对枚举类型的值进行比较。比如,在下述代码中,Monday(作为Day类型的'First)和Sunday(作为Day类型的'Last)被比较:

if Mo < Su then
    Ada.Text_IO.Put("Monday < Sunday");
end if;

3.9 标准类型的选择

有关标准类型,下面提供了三种定义方式,并讨论了哪种更好:

type SecondOfDay is range 0 .. 86_400;               -- Option 1
type SecondOfDay is new Integer range 0 .. 86_400;    -- Option 2
subtype SecondOfDay is Integer range 0 .. 86_400;     -- Option 3
  • Option 1:这是最佳选项,因为它定义了一个新的类型,范围是0到86400。这种方式最具有可移植性,因为这个类型不依赖于Integer类型的具体实现。

  • Option 2:这个定义创建了一个新的类型,它是Integer类型的子类型,范围是0到86400。但是这种定义的可移植性不如Option 1,因为这个类型的具体实现取决于Integer类型的实现。

  • Option 3:这个定义创建了一个名为SecondOfDay的子类型,它是Integer类型的一个子集,范围是0到86400。这种定义的静态检查能力不如Option 1和Option 2,因为子类型的值可以被隐式地转换为其基类型的值,这可能会引发类型范围外的错误。

因此,如果你需要定义一个在特定范围内的类型,使用Option 1的方式是最好的。

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

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

相关文章

Java jvm调优

系列文章目录 文章目录 系列文章目录前言JVM 基础面试题11. JDK&#xff0c;JRE以及JVM的关系2. 我们的编译器到底干了什么事&#xff1f;3. 类加载机制是什么&#xff1f;3.1 装载(Load)3.2 链接(Link)验证(Verify)准备(Prepare)解析(Resolve) 3.3 初始化(Initialize) 4. 类加…

chatgpt赋能python:Python三次幂与其应用

Python三次幂与其应用 Python是一种高级编程语言&#xff0c;因其简单易用的语法和广泛应用而备受欢迎。在该语言中&#xff0c;三次幂是其中一个常用操作之一。本文将介绍Python三次幂的概念及其应用&#xff0c;为您带来有价值的参考。 什么是Python三次幂&#xff1f; Py…

KubeSphere 社区双周报 | 杭州 Meetup 报名中 | 2023.05.12-05.25

KubeSphere 社区双周报主要整理展示新增的贡献者名单和证书、新增的讲师证书以及两周内提交过 commit 的贡献者&#xff0c;并对近期重要的 PR 进行解析&#xff0c;同时还包含了线上/线下活动和布道推广等一系列社区动态。 本次双周报涵盖时间为&#xff1a;2023.05.12-2023.…

Linux - Java 8 入门安装与重装教程集锦

一、入门初始安装 1. 具体安装教程 1. linux 系统中如何安装java环境&#xff08;通过tar.gz文件&#xff09; 安装包下载链接 Java 的 tar.gz 安装包下载链接传送门 Linux 系统的 Java 环境变量配置教程 1. linux查看java版本&#xff0c;以及配置java home 2. Linux环…

stackqueue

这篇主要讲栈(stack)和队列(queue)&#xff0c;实际要学习的数据结构有三个&#xff1a;stack、queue、priority_queue 这些数据结构已经不属于容器了&#xff0c;而是容器适配器。 list的第二个参数是空间配置器&#xff0c;支持申请空间&#xff1b;而list和queue的第二个参…

Windows下利用Anaconda创建多个CUDA环境

参考 https://blog.csdn.net/qq_42395917/article/details/126237388 https://blog.csdn.net/qq_42406643/article/details/109545766 (待学习补充) https://blog.csdn.net/qq_43919533/article/details/125694437 (待学习补充) 安装cudatoolkit和cudnn # 前提是我已经安装了…

【Python 打包应用发布程序】零基础也能轻松掌握的学习路线与参考资料

Python是一种流行的编程语言&#xff0c;因其易学易用、灵活和高效而受到广泛关注和应用&#xff0c;尤其是在开发Web应用、数据科学和人工智能方面。Python的强大之处在于其丰富的第三方库和工具&#xff0c;可以让开发者轻松地构建复杂的应用程序和脚本工具。但是&#xff0c…

完全掌握git入门到精通各类免费书籍整理

大型软件项目开发&#xff0c;多人群组开发都离不开的版本控制工具 git&#xff0c;命令简单&#xff0c;想要完全掌握却需要付出一点时间。我们将一些评价较高的git免费学习资料网站做了整理&#xff0c;收录到 学习使用git完全指南各种免费书籍分享 完全掌握git入门到精通各…

【IDEA插件开发】快速入门系列01 开发一个简单的Idea插件

IDEA插件开发流程 IDEA插件开发官方文档 英文好的建议阅读官方文档 IDEA插件开发官方文档&#xff1a;https://plugins.jetbrains.com/docs/intellij/welcome.html 搭建IDEA插件开发环境 1.安装社区版IDEA 在这里我们需要下载IDEA社区版的历史版本。 历史版本的下载网址&a…

自学黑客?一般人我劝你还是算了吧

博主本人 18年就读于一所普通的本科学校&#xff0c;21年 6 月在三年经验的时候顺利通过校招实习面试进入大厂&#xff0c;现就职于某大厂安全联合实验室。 我为啥说自学黑客&网络安全&#xff0c;一般人我还是劝你算了吧。因为我就是那个不一般的人。 首先我谈下对黑客&am…

Java日期时间调整的几种方式

一、Calendar类 我们现在已经能够格式化并创建一个日期对象了&#xff0c;但是我们如何才能设置和获取日期数据的特定部分呢&#xff0c;比如说小时&#xff0c;日&#xff0c;或者分钟? 我们又如何在日期的这些部分加上或者减去值呢? 答案是使用Calendar 类。 Calendar类的…

六、基本数据类型

数据类型 一、基本数据类型 以下是go中可用的基本数据类型 1.1 布尔型bool 布尔型的值只可以是常量 true 或者 false。一个简单的例子&#xff1a;var b bool true 1.2 数值型 1、整数型 int8 有符号 8 位整型 (-128 到 127) 长度&#xff1a;8bit int16 有符号 16 位整…

jmeter接口工具使用详解之基础介绍

目录 一、优点 二、安装及下载 三、基础构成 jmeter是一款优秀的开源性能测试工具&#xff0c; 一、优点 1、开源工具&#xff0c;可扩展性非常好 2、高可扩展性&#xff0c;用户可自定义调试相关模块代码 3、精心简单的GUI设计&#xff0c;小巧灵活 4、完全的可移植性…

电子科技大学编译原理复习笔记(五):词法分析

目录 前言 重点一览 词法分析概述 词法分析的功能 词法分析器的输出形式 词法分析器的结构 状态转换图 状态转换图的构造 词法分析器的设计 基本结构 内容 符号表 目的 组成 在词法分析中的作用 符号表的一般形式 常用的符号表结构 总结与补充 为何分离词法…

小学百分数思维导图怎么画?这样制作不出错

百分数是数学中的一个重要概念&#xff0c;它用于表示一个数在另一个数中所占的比例。在日常生活中&#xff0c;我们经常使用百分数进行计算和比较。而百分数思维导图是一种图形化的表示方法&#xff0c;用于展示数值之间的比例关系。它通过将数值转化为百分数的形式&#xff0…

python学习——描述统计df.describe

文章目录 1 描述统计1.1 查看常见统计量 describe1.2 一般对数值型数据统计1.2.1 基于非空数值统计sum\mean\max\min\var\std1.2.2 每一列中最大值的行索引 idxmax1.2.3 每一行中最大值的列索引 idxmax&#xff08;axis 1&#xff09;1.2.4 非空的数量 count() 1.3 一般对字符…

Sugar BI 预测服务:快速通过机器学习,进行数据预测分析

什么是预测服务&#xff1f; 机器学习是一门关于数据学习的科学技术&#xff0c;它能帮助机器从现有的复杂数据中学习规律&#xff0c;以预测未来的行为结果和趋势。 Sugar BI 作为对数据进行分析的可视化平台&#xff0c;也支持用户对自己的数据使用机器学习算法进行探索试分…

赛灵思 ZYNQ UltraScale+ MPSoC Petalinux驱动开发:Linux字符驱动开发

目录 赛灵思 ZYNQ UltraScale MPSoC&#xff1a;Linux字符驱动开发1、Linux驱动程序简介2、Linux字符设备开发步骤2.1、系统调用2.2、驱动模块的加载与卸载2.2.1、驱动加载/卸载方式&#xff1a;2.2.2、驱动注册函数和卸载注册函数2.2.3、字符设备注册与注销2.2.4、实现设备操作…

遥感云大数据在灾害、水体与湿地领域典型案例实践及GPT模型应用

近年来遥感技术得到了突飞猛进的发展&#xff0c;航天、航空、临近空间等多遥感平台不断增加&#xff0c;数据的空间、时间、光谱分辨率不断提高&#xff0c;数据量猛增&#xff0c;遥感数据已经越来越具有大数据特征。遥感大数据的出现为相关研究提供了前所未有的机遇&#xf…

GRPC C++ windows下的简易安装方法

最近因为想给Llama.cpp加一个grpc入口&#xff0c;折腾了一圈GRPC运行时的安装&#xff0c;起初参考GRPC官方的Build from source&#xff0c;未果。 主要原因是基于cmake的安装和调用遭遇到几次大的问题。 一是vscode编译器集成的问题&#xff0c;二是cmake的find_package的…