问题标签 [ada2012]

Spark 的新手，Ada 的新手，所以这个问题可能过于宽泛。但是，作为理解 Spark 的尝试的一部分，它是真诚地询问的。除了直接回答以下问题外，我还欢迎对风格、工作流程等提出批评。

作为我第一次涉足 Spark，我选择尝试实现（简单）并证明正确性（迄今为止不成功）该功能。

问题：实现和证明此功能正确性的正确方法是什么？

我从以下开始util.ads：

我没有先决条件，因为输入的范围完全表达了唯一有趣的先决条件。我根据数学定义写的后置条件；但是，我在这里有一个直接的担忧。如果X是Positive'Last，则2**(Floor_Log2'Result + 1)超过Positive'Last和Natural'Last。我已经在这里反对我对 Ada 的有限知识，所以：子问题 1：后置条件中子表达式的类型是什么，这是溢出问题吗？有没有通用的方法来解决它？为了避免这种特殊情况下的问题，我将规范修改为不太直观但等效的：

有很多方法可以实现这个功能，我现在并不特别关心性能，所以我对其中任何一种都很满意。我认为“自然”实现（鉴于我特定的 C 背景）类似于以下内容util.adb：

正如预期的那样，尝试在没有循环不变量的情况下证明这一点会失败。结果（此结果和所有结果均为 GNATprove 级别 4，从 GPS 调用为gnatprove -P%PP -j0 %X --ide-progress-bar -u %fp --level=4 --report=all）：

这里的大多数错误对我来说都是基本的。从第一次溢出检查开始，GNATprove 无法证明循环在少于Natural'Last迭代次数（或根本没有？）内终止，因此它无法证明I := I + 1没有溢出。我们知道情况并非如此，因为Remaining正在减少。我试图通过添加循环变体来表达这一点pragma Loop_Variant (Decreases => Remaining)，并且 GNATprove 能够证明循环变体，但潜在的溢出I := I + 1没有改变，推测是因为证明循环完全终止并不等于证明它在少于Positive'Last迭代中终止。更严格的约束将表明循环最多在Positive'Size迭代中终止，但我不确定如何证明这一点。相反，我通过添加一个“强迫它”pragma Assume (I <= Remaining'Size); 我知道这是不好的做法，这里的目的纯粹是为了让我看看我能在第一期“被掩盖”的情况下走多远。正如预期的那样，这个假设让证明者可以证明实现文件中的所有范围检查。子问题2：证明I在这个循环中不溢出的正确方法是什么？

但是，我们在证明后置条件方面仍然没有取得任何进展。显然需要循环不变量。保持在循环顶部的一个循环不变量是pragma Loop_Invariant (Remaining * 2**I <= X and then X/2 < Remaining * 2**I); 除了为真之外，该不变量还有一个很好的特性，即当循环终止条件为真时，它显然等同于后置条件。然而，正如预期的那样，GNATprove 无法证明这个不变量：medium: loop invariant might fail after first iteration, cannot prove Remaining * 2**I <= X[#20]. 这是有道理的，因为这里的归纳步骤是不明显的。通过对实数进行除法，可以想象一个简单的引理说明for all I, X * 2**I = (X/2) * 2**(I+1)，但是（a）我不希望 GNATprove 在没有提供引理的情况下知道这一点，并且（b）整数除法更加混乱。那么，子问题 3a：这是尝试用来证明此实现的适当循环不变量吗？子问题 3b：如果是这样，证明它的正确方法是什么？从外部证明一个引理并使用它？如果是这样，那究竟是什么意思？

在这一点上，我想我会探索一个完全不同的实现，只是看看它是否会导致不同的地方：

这对我来说是一个不太直观的实现。我没有过多地探索第二个实现，但我把它留在这里展示我尝试了什么；为主要问题的其他解决方案提供潜在途径；并提出额外的子问题。

这里的想法是通过明确终止和范围来绕过 I 和终止条件溢出的一些证明。令我惊讶的是，证明者首先在溢出检查表达式时窒息2**I。我曾期望2**(X'Size - 1)可以证明在范围内X——但我又一次遇到了我的 Ada 知识的限制。子问题 4：这个表达式在 Ada 中实际上是无溢出的吗？如何证明？

事实证明这是一个很长的问题......但我认为我提出的问题，在一个几乎微不足道的例子的背景下，是相对普遍的，并且可能对像我一样试图尝试的其他人有用了解 Spark 是否以及如何与他们相关。

我正在处理一个具有重大 RAM 限制的遗留 Ada 项目。

为了节省额外功能的内存，我想分析所有记录定义，以便：

1. 检测漏洞（即浪费的字节）
2. 提出一个最小化内存占用的记录声明顺序（或表示）（使用一些应该类似于背包问题的算法）

请注意，我（还没有）在保存任何丢失的位的过程中（这里不需要，也不需要 rep. 子句，用于像这个问题pragma pack中的严格连续的记录）。现在只有字节。

简化示例（真实世界记录要复杂得多，可能有判别式、标记类型）：

它的-gnatR2s输出看起来像（32 位世界）：

我想做什么（内存使用优化记录）：

或者：

（为示例中的任何错误道歉，我希望你明白这一点）

我怎样才能做到这一点 ？

1. ASIS（但我的技能为 0%，我什至不确定它是否能做我想做的事）
2. libadalang（如何在不编译单元的情况下获得代表条款？）
3. 只需-gnatR2s在所有编译单元上使用并在 python 中编写.rep解析器
4. 有一个隐藏的编译选项，一个 pragma 或现有的 GNAT 工具可以提供帮助（如pragma component_alignment或pragma optimize_alignment，但我不能说他们是否解决了这个问题，因为它会影响对齐，但不一定是对齐 + 排序)

有关 repl 子句、Ada 参考手册和 GNAT 小差异的上下文，可以阅读此链接

我正在尝试将一个结构从（x86）汇编程序传递给堆栈上的 Ada。我已经能够在 C 中成功地使用这种模式来接受将从程序集传递的大量参数包装在一个结构中，我想知道这是否会在 Ada 中以类似的方式工作。

这是一个（人为的，最小的）示例：

当我这样做时，调试被调用者显示传递的记录包含未初始化的数据。尽管有导出指令，但 Ada 似乎对 C 调用约定的解释不同。RM 包含有关将结构从 Ada 传递到 C 的信息，表示它将自动将记录作为指针类型传递，但反过来似乎并不成立。如果您接受单一access类型，它将简单地填充堆栈上的第一个值，正如人们对 cdecl 所期望的那样。

（请原谅任何小错误，这不是我的实际代码。）

另一方面，这工作得很好：

在这个最小的情况下，这没什么大不了的，但如果我传递 16 个或更多变量，它会变得有点繁重。如果您想知道我为什么要这样做，它是一个异常处理程序，处理器会自动将变量传递到堆栈以显示寄存器状态。

在这里的任何帮助将不胜感激。

Context

I recently came into a basic OOP / Ada 2012 design issue.

Basically, I have a parent class that realizes an interface contract. This is done in several steps inside an implementation provider (ConcreteX). A child class extends this implementation by overriding only one of the steps (DerivedY, Step_2). (trying to get some SOLID properties)

I naively assumed that dispatching would occur. It doesn't. I rediscovered that dispatching is NOT like in Java or other OOP, and have come with a solution.

Dispatching in Ada is frequently asked/answered/documented in several questions: Dynamic dispatching in Ada, Dynamic Dispatching in Ada with Access Types, Fundamentals of Ada's T'Class

Instead of using:

I ended up using:

Question

Within an Ada OOP class design, I'm struggling between those two choices:

1. In the parent class, define behavior + primitives and provide a default implementation i.e. Current_Class'Class(This).method() (= working example provided below)

2. Use a template design pattern so execution steps implementation is delegated to another class

i.e. in the given example:

Is 1 a syntaxic "trick" that should be avoided to achieve the intended behavior?

I always feel like when I write an explicit cast, that's a sign of weak design.

Working example:

src/interfacea.ads

src/concretex.ads

src/concretex.adb

src/concretex-derivedy.ads

src/concretex-derivedy.adb

src/main.adb

inheritanceanddispatch.gpr

Gnat versions:

Output:

在开发 QR 码生成器的早期阶段，我遇到了来自 GNAT 7.4.0（在“Ubuntu 19.04”系统上运行）的特殊“信息”消息。

我正在使用一些相当激进的编译开关：

我的代码确实没有错误地构建，但此信息消息确实表明我没有为包“qr_symbol”提供正文。

qr_symbol.ads

qr_symbol.adb

这是我不明白的信息输出......

程序输出（给定正确的输入，确实给出正确的输出）...

问题： 为什么有一条信息消息提示我需要为这个包提供一个主体，而我已经这样做了？

我已经从 Github 下载了这个程序：https ://github.com/raph-amiard/ada-synth-lib

我已经尝试了第一个示例，但遇到了一个例外。如果有人能够让我深入了解为什么会这样，将不胜感激。我已经为此困扰了很长时间，我真的很想让它发挥作用。

我收到的错误是：raised PROGRAM_ERROR : waves.adb:110 accessibility check failed

这是主文件：

这是waves.adb文件

最后，write_to_stdout.adb 文件

感谢您的阅读，任何解决此问题的指导都将是最受赞赏的。

干杯，

劳埃德

我之前问过一个关于在 Ada 中提出的可访问性检查的问题，@Brian Drummond 很友好地接受了 awnser。可访问性检查在一个函数中，现在我在一个过程中有一个类似的问题；任何关于为什么会这样的指导将不胜感激。

我正在处理的代码取自这里：https ://github.com/raph-amiard/ada-synth-lib

下面主文件中的代码来自 Simple_Sine 示例，可在此处找到： https ://github.com/raph-amiard/ada-synth-lib/blob/master/examples/simple_sine.adb

我的主文件如下所示：

引发的错误是这样的： raised PROGRAM_ERROR : sound_gen_interfaces.adb:20 accessibility check failed

它在调用此过程期间引发：

这是下面代码的第 20 行：

任何有关为什么会发生这种情况的帮助将不胜感激。

谢谢

我最近在我的 Linux 机器（Centos7）上下载了 GNAT 社区。

在 /home/parallels/opt/GNAT/2019 中有一个文件夹 gprbuild，我的理解是要安装它，我需要执行位于 gprbuild 中的 bootstrap.sh 脚本：/home/parallels/opt/GNAT/2019/ gprbuild/bootstrap.sh

我尝试像这样执行 bootstrap.sh 脚本......

[parallels@localhost gprbuild]$ ./bootstrap.sh

然后我收到此错误消息...

./bootstrap.sh: line 87: gnatmake: command not found

这是 bootstrap.sh 脚本...

有人告诉我，我需要在安装 gprbuild 之前安装 xmlada，然后我在其他地方读到我需要安装 gprbuild 才能安装 xmlada！

我在尝试安装 xmlada 时遇到了类似的问题，xmlada 文件夹中的 shell 脚本称为 install-sh，当我尝试安装它时，我被告知没有指定输入文件...

我知道这确实是两个问题，但我觉得我必须这样解释，因为我不确定首先需要安装哪个库，以及如何实际安装它们。

任何帮助将不胜感激！我希望你们都度过了一个愉快的周末...... :)

谢谢，劳埃德

我最近开始在 GNAT GPS 社区版中使用 gnatcoll、gnatcoll_sql、gnatcoll_postgres 库。

我的 default.gpr 文件看起来像这样..

我的主文件看起来像这样

当我执行时，我收到以下错误消息...

我怀疑是否尝试更改此代码，因为它位于 gnatcoll 库中。gnatcoll-strings_impl.ads如果我应该更改&内的代码，请谁能告诉我gnatcoll-sql.ads或者有其他解决方案吗？

我无法包含下面的gnatcoll-strings_impl.ads&gnatcoll-sql.ads文件以供参考，因为它们太大了！这里有一些屏幕截图供参考...

添加于 2020 年 4 月 29 日

添加于 2020 年 2 月 5 日

我正在尝试使用 GNAT CE 2019 查询 PostgreSQL 数据库。我的数据库中有两个表，汽车和人员：

我想执行一个简单的 Select 语句，当我在终端中使用 psql 执行此操作时，返回的是：

但是，我想在 GNAT CE 2019 中执行此操作。这是我的 main.adb 文件当前的外观：

尝试建立与数据库的连接时，进程成功终止。

我不确定应该用于 Select 语句的语法。如果有人能够告诉我如何SELECT * FROM Person;在 GNAT CE 2019 中执行简单的语句，将不胜感激。

谢谢你，劳埃德

添加于 20 年 13 月 5 日

添加于 15/05/20

添加于 20 年 5 月 17 日

添加于 2020 年 5 月 29 日