高完整性系统工程(六):INTRODUCING ADA

news2024/12/25 10:30:31

目录

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/600225.html

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

相关文章

IPython使用学习笔记

学习《利用python进行数据分析》第三章 IPython:一种交互式计算和开发环境的笔记&#xff0c;共享给大家&#xff0c;同时为自己作为备忘用。 安装ipython用pip即可。ps.博主用的是win7系统&#xff0c;所以接下来的都是在windows系统下操作的。 一.Ipython基础 启动&#xff…

chatgpt赋能python:Python关闭程序代码的实现方法

Python 关闭程序代码的实现方法 如果你是一个经验丰富的 Python 工程师&#xff0c;你应该知道如何在程序中实现正常关闭。不过&#xff0c;如果你是一个新手&#xff0c;这可能会变得有点棘手&#xff0c;特别是当你需要在程序中添加一些特定的关闭功能的时候。本文将为您介绍…

【javaEE】计算机网络原理初始

目录 1、网络发展史 1.1、独立模式 1.2、网络互连 1.2.1、局域网&#xff08;LAN&#xff09; 1.2.2、广域网&#xff08;WAN&#xff09; 1.2.3、广域网和局域网的区别 1.2.4、局域网组建网络的方式 &#xff08;了解&#xff09; &#xff12;、网络通信基础 2.1、I…

前端开发技术栈(工具篇):2023最新版nvm的Win/Linux安装和使用(详细) 27.8k stars

目录 nvm是什么 nvm下载 nvm安装 Windows nvm的使用 安装Node.js 切换Node.js版本 卸载Node.js 其他使用方法 Linux nvm的使用 安装NVM 使用NVM 总结 Node.js是一个非常流行的JavaScript运行时环境&#xff0c;可以帮助开发人员构建高性能的网络应用程序, 它被用于…

SpringCloud:分布式锁和线程安全

这篇文章是一个初步了解分布式应用的线程安全和锁的文章&#xff0c;所有截图及代码全部来自亲身实践 1.对于单机应用我们可以把锁加在方法维度&#xff08;有用&#xff0c;不推荐&#xff09; 像这样 但是我们应该缩小锁的范围&#xff0c;我们这里是在派单&#xff0c;避免…

手撕希尔排序

什么是希尔排序&#xff1f;他的效率怎摸样&#xff0c;如何去实现希尔排序呢&#xff1f;在这之前可能我们已经了解了希尔排序&#xff0c;作为排序中的老大哥一员&#xff0c;希尔排序的效率也是屈指可数的。 想要知道希尔排序如何实现我们就的先了解插入排序。 目录 1.何…

Flutter 笔记 | Flutter 核心原理(六)Embedder 启动流程(Android)

Embedder是Flutter接入原生平台的关键&#xff0c;其位于整个Flutter架构的底层&#xff0c;负责Engine的创建、管理与销毁&#xff0c;同时也为Engine提供绘制UI的接口&#xff0c;那么底层的实现细节如何&#xff1f;本文将详细分析。 Embedder关键类分析 在正式分析Embedd…

chatgpt赋能python:Python知识|关联两个列表

Python 知识 | 关联两个列表 Python 是一种高效的编程语言&#xff0c;它能够很好地进行数据处理&#xff0c;因此在 SEO 领域得到广泛的应用。关联两个列表是一种基础的数据处理方法&#xff0c;本文将为读者详细介绍如何使用 Python 关联两个列表&#xff0c;并给出一些实例…

Rust每日一练(Leetday0018) N皇后II、最大子数组和、螺旋矩阵

目录 52. N皇后 II N Queens II &#x1f31f;&#x1f31f;&#x1f31f; 53. 最大子数组和 Maximum Subarray &#x1f31f;&#x1f31f; 54. 螺旋矩阵 Spiral Matrix &#x1f31f;&#x1f31f; &#x1f31f; 每日一练刷题专栏 &#x1f31f; Rust每日一练 专栏…

chatgpt赋能python:Python关键词匹配:优化你的SEO策略

Python关键词匹配&#xff1a;优化你的SEO策略 在当今数字时代&#xff0c;搜索引擎是许多人获取信息和发现新客户的主要渠道。对于企业或个人网站来说&#xff0c;优化SEO&#xff08;搜索引擎优化&#xff09;策略变得至关重要。在SEO的世界里&#xff0c;关键词匹配是一个重…

springboot+vue编程训练考试测试系统设计与实现

本编程训练系统管理员功能有管理员和用户。管理员功能有个人中心&#xff0c;用户管理&#xff0c;题库资源管理&#xff0c;用户交流&#xff0c;试卷管理&#xff0c;留言板管理&#xff0c;试题管理&#xff0c;系统管理&#xff0c;考试管理。用户可以查看题库资源&#xf…

chatgpt赋能python:使用Python进行人民币兑换-带着您深入了解

使用Python进行人民币兑换 - 带着您深入了解 在当今日益全球化的世界里&#xff0c;进行货币兑换已成为很正常的事情。人民币是世界上最常用的货币之一&#xff0c;而Python作为一种强大的编程语言&#xff0c;可以帮助我们进行人民币兑换计算。本文将介绍如何使用Python进行人…

使用CCProxy搭建windows系统阿里云socket代理服务器 教程

目录 1. 通过windows远程连接阿里云服务器2. 云服务器上安装CCProxy2.1 CCProxy下载安装2.2 设置协议、代理服务、端口号和ip2.3 新建代理用户2.4 确保你的CCProxy启动了服务 3. 在阿里云实例安全组中开放代理端口3.1 前往安全组页面3.2 添加你对应服务的开放端口 总结 欢迎关注…

Java键盘事件处理及监听机制解析

文章目录 概念KeyEventKeyListener代码演示总结 概念 Java事件处理采用了委派事件模型。在这个模型中&#xff0c;当事件发生时&#xff0c;产生事件的对象将事件信息传递给事件的监听者进行处理。在Java中&#xff0c;事件源是产生事件的对象&#xff0c;比如窗口、按钮等&am…

java企业级信息系统开发学习笔记11 利用MyBatis实现条件查询

文章目录 一、学习目标1.对学生表进行条件查询&#xff0c;涉及姓名、性别和年龄三个字段。2.比如查询姓“吴”&#xff0c;性别为“女”&#xff0c;同时年龄为19的学生记录 二、打开上一笔记mybatis项目三、对学生表实现条件查询&#xff08;一&#xff09;创建学生映射器配置…

如何使用wget下载(录制)流媒体或直播推流文件,以及下载出现“正在把输出重定向至 “wget-log.1””错误该怎么办

下载推流文件其实非常简单&#xff0c;就是通常使用的最简单的命令&#xff1a; wget URL -O 输出文件名这里最好设置一下输出文件名&#xff0c;不然很可能下载的文件名称会很奇怪&#xff0c;导致格式识别错误或者其他问题。 不过&#xff0c;如果你直接使用这个命令很可能…

微信小程序nodejs+vue图书馆自习室座位管理系统vax51

系统设计需要从用户和管理员的实际需求开始&#xff0c;以了解他们需要实施哪些功能以及他们可以包括哪些管理工作。 考虑到图书馆座位预约系统小程序系统设计的特点&#xff0c;应满足几个要求&#xff1a;开发语言 node.js 框架&#xff1a;Express 前端:Vue.js 数据库&#…

[MySQL从入门到精通]MySQL概述及安装

前言 你是否想过我们在登录各种各样的网站时候&#xff0c;所需要输入的账号密码&#xff0c;它们存储在哪里&#xff1f;你猜对了&#xff0c;就是今天我们所要说的数据库 目录 前言 1.数据库的概述 1.1 数据 1.2 数据库 1.3数据库的种类 1.4数据库管理系统 2.MySQL的…

CSS 水平垂直居中的方式

目录 在不知道子元素宽高的情况下&#xff0c;水平垂直居中的六种方式&#xff1a; 1、弹性盒子布局方式来实现&#xff08;flex&#xff09;。 2、绝对定位 transform 3、table标签 4、display&#xff1a;table-cell 5、display: grid 6、writing-mode 属性 在不知道子…

chatgpt赋能python:10年Python编程经验的工程师推荐:免费的PythonIDE

10年Python编程经验的工程师推荐&#xff1a;免费的Python IDE 作为一名有着10年Python编程经验的工程师&#xff0c;我一直在寻找可以帮助我提高效率的Python IDE。在这个过程中&#xff0c;我试用了许多付费和免费的IDE&#xff0c;最终发现了一些免费的Python IDE&#xff…