标签: ada2012

Spark的新手,Ada的新手,所以这个问题可能过于宽泛.然而,作为尝试理解Spark的一部分,它是出于善意的要求.除了下面问题的直接答案,我欢迎对风格,工作流程等的批评.

作为我第一次涉足Spark,我选择尝试实现(简单)并证明正确性(迄今为止不成功)的功能 .

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

我从以下开始util.ads:

package Util is
   function Floor_Log2(X : Positive) return Natural with
     Post => 2**Floor_Log2'Result <= X and then X < 2**(Floor_Log2'Result + 1);    
end Util;

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

package Util is
   function Floor_Log2(X : Positive) return Natural with
     Post => 2**Floor_Log2'Result <= X and then X/2 < 2**Floor_Log2'Result;
end Util;

有很多方法可以实现这个功能,我现在并不特别关注性能,所以我对它们中的任何一个都很满意.我认为"自然"实现(鉴于我的特定C背景)如下所示util.adb:

package body Util is
   function Floor_Log2 (X …

不使用 nonstandard\xe2\x80\xa1 Scalar_Storage_Order 子句，如何通过记录表示子句结合任何其他语言功能的任意组合来可移植地表示 IPv4 标头，以便 \ xe2\x80\x9c相同的\xe2\x80\x9d 代码适用于小端和大端处理器，但以 IETF 称为网络字节的方式在线上发出（例如，通过以太网帧的有效负载） order（这是 IETF 对 big-endian 的奇特名称）。在 C 中，\xe2\x80\x9c相同的\xe2\x80\x9d 代码可以利用预处理器宏在小端处理器上执行字节交换，但在大端处理器上不执行任何操作，但标准 Ada 没有预处理器。在 C++ 中，\xe2\x80\x9c相同的\xe2\x80\x9d 代码可以利用元模板编程 (MTP) 在小端处理器上执行字节交换，但在大端处理器上不执行任何操作，但是标准 Ada 缺乏 MTP。

（顺便说一句，当大端处理器与小端外设 IC 的内存映射寄存器接口时，设备驱动程序中也会出现同样的问题，反之亦然：小端处理器与大端 IC 接口时的内存映射寄存器。）

    BytesPerWord : constant := 4;\n    BitsPerByte : constant := 8;\n    PowerOf2Highest : constant := BytesPerWord*BitsPerByte - 1; -- part #1 of byte-swap\n    type Header_IPv4 is record\n          Version   : integer range 0 ..    F#16;\n          IHL       : integer range 0 ..    F#16;\n          TOS       : integer …

我正在尝试从许多月前做一些旧C++代码的基本翻译来学习Ada,我一直对如何使用内置Generic_Sorting对矢量进行排序感到困惑.我还没有找到任何具体的实际例子,最接近现在已经不复存在的丹麦维基文章看起来好像有一个完整的例子,但存档没有抓住它:https:// web.archive.org/web/20100222010428/http://wiki.ada-dk.org/index.php/Ada.Containers.Vectors#Vectors.Generic_Sorting

这是我认为应该从上面的链接工作的代码:

with Ada.Integer_Text_IO;    use Ada.Integer_Text_IO;
with Ada.Strings.Unbounded;  use Ada.Strings.Unbounded;
with Ada.Containers.Vectors; use Ada.Containers;

procedure Vectortest is
   package IntegerVector is new Vectors
     (Index_Type   => Natural,
      Element_Type => Integer);
   package IVSorter is new Generic_Sorting;

   IntVec : IntegerVector.Vector;
   Cursor : IntegerVector.Cursor;
begin
   IntVec.Append(3);
   IntVec.Append(43);
   IntVec.Append(34);
   IntVec.Append(8);

   IVSorter.Sort(Container => IntVec);

   Cursor := IntegerVector.First(Input);
   while IntegerVector.Has_Element(Cursor) loop
      Put(IntegerVector.Element(Cursor));
      IntegerVector.Next(Cursor);
   end loop;

end Vectortest;

我试过这么多不同的组合use和with,但所有我能得到的各种错误代码.上面的代码给出了Generic_Sorting is not visible,但是当我尝试明确说明with Ada.Containers.Vectors.Generic_Sorting我得到了错误"Ada.Containers.Vectors.Generic_Sorting" is not a predefined library …

如果没有在这里复制粘贴我的代码，如果它计算出“ X”的某个值，如何在运行时停止ADA程序执行代码行？

就像是：

 variable_name := variable_name +4;
 if variable_name >1 then
 // END program here and dont execute any lines under this one
 end if

我不是编程新手，而是ADA新手，所以找到正确的语法很痛苦。有什么帮助吗？

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

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

gnatmake -gnata -gnateE -gnateF -gnatf -gnato -gnatv -gnatVa -gnaty -gnatwe -gnatw.e main.adb

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

qr_symbol.ads

with QR_Versions; use QR_Versions;

generic
   Ver : QR_Version;
package QR_Symbol is
   procedure Export_As_SVG;
private
   type Module_State is (
     Uncommitted,
     One,
     Zero
     );

   type Module_Family is (
     Uncommitted,
     Finder,
     Separator,
     Alignment,
     Timing,
     Format_Spec,
     Version_Spec,
     Data_Codeword,
     EC_Codeword,
     Padding
     );

   type Module is
      record
         State : Module_State := Uncommitted;
         Family : Module_Family := Uncommitted;
      end record;

   type Module_Matrix is array (
     Positive …

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

我尝试了第一个例子，但遇到了一个例外。如果有人能够让我深入了解这是为什么，我将不胜感激。我已经被这个问题困扰了很长时间，而且我真的很渴望让它发挥作用。

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

这是主要文件：

with Waves; use Waves;
with Write_To_Stdout; 



procedure Main is



   Sine_Gen : constant access Sine_Generator := Create_Sine (Fixed (440.0));

begin


  Write_To_Stdout (Sine_Gen);


end Main;

这是waves.adb 文件

with Effects; use Effects;
with Interfaces; use Interfaces;

package body Waves is

   function Mod_To_Int (A : Unsigned_32) return Integer_32;

   -------------------
   -- Update_Period --
   -------------------

   procedure Update_Period
     (Self : in out Wave_Generator'Class; Buffer : in out Period_Buffer)
   is
   begin
      Self.Frequency_Provider.Next_Samples (Buffer); …

我正在实例化一个带有枚举的通用包，以访问多个值之一并在子程序重载中使用。我想要一个定义明确的、编译时检查过的值集，我可以使用和查找。

generic
    -- Different types because we don't want to ensure we never put
    -- beer in a wine class, or wine in a beer stein.  Our inventory
    -- never changes, for... reasons.
    type Wine is (<>);
    type Beer is (<>);
package Bar is
    type Wine_Glass is null record;
    type Beer_Stein is null record;

    -- Unopened cases/bottles of each.
    type Wine_Inventory is array (Wine) of Natural;
    type Beer_Inventory is array (Beer) of Natural;

    procedure Pour (G : in out Wine_Glass; …

语境

我最近遇到了一个基本的OOP / Ada 2012设计问题。

基本上，我有一个实现接口协定的父类。这是在实现提供程序（ConcreteX）中分几个步骤完成的。子类通过仅覆盖其中一个步骤（DerivedY，Step_2）来扩展此实现。（试图获得一些SOLID属性）

我天真地认为会发生调度。没有。我重新发现调度与Java或其他OOP中的调度不同，并提供了解决方案。

在阿达调度经常问/回答/记录了几个问题：动态调度Ada中，动态调度Ada中，访问类型，阿达T'Class基础

而不是使用：

This.Step_1; This.Step_2;

我最终使用：

T_Concrete_X'Class (This).Step_1; T_Concrete_X'Class (This).Step_2;

题

在Ada OOP类设计中，我在两种选择之间挣扎：

1. 在父类中，定义行为+原语并提供默认实现，即Current_Class'Class(This).method()（=下面提供的工作示例）

2. 使用模板设计模式，以便将执行步骤的实现委派给另一个类

即在给定的示例中：

-- T_Concrete_X does not have a child class (current example)
overriding procedure If_A_Proc_1 (This : in out T_Concrete_X) is
begin
   -- This.template_executor being set with different classes realizing the Step_1/Step_2 contracts(current example)
   This.template_executor.Step_1;
   This.template_executor.Step_2;
end If_A_Proc_1;

1是应避免达到预期行为的语法“技巧”吗？

我总是觉得当我写一个显式的演员表时，那是设计不力的标志。

工作示例：

src / interfacea.ads

package InterfaceA is

   type T_InterfaceA is interface;
   type T_InterfaceA_Class_Access …

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

mydb1-# \dt
         List of relations
 Schema |  Name  | Type  |  Owner   
--------+--------+-------+----------
 public | car    | table | postgres
 public | person | table | postgres
(2 rows)

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

mydb1=# SELECT * FROM Person;

              person_uid              | first_name | last_name  | gender |            email             | date_of_birth | country_of_birth |               car_uid                
--------------------------------------+------------+------------+--------+------------------------------+---------------+------------------+--------------------------------------
 75f5e55d-12b2-463e-93ff-1c921e44c3e1 | Audrie     | Vasyukov   | Female | avasyukovd6@domainmarket.com | 1988-11-24    | Guatemala        | 
 9e3f7f90-6e9a-4f2d-ae4e-c852d819ed33 | …

我的类型类似于:

type ID is new String (1 .. 7);
-- Example: 123-456

如何使用Ada或SPARK在代码中指定该格式？

我在考虑Static_Predicate,但是字符串必须以3个正整数开头,然后是破折号后跟另一组3个正整数的条件不能用Static_Predicate表达式来描述.

如果断言失败，我会得到以下输出：

引发 SYSTEM.ASSERTIONS.ASSERT_FAILURE ：Dynamic_Predicate 在 file.adb:36 处失败

我能得到更多细节吗？例如输入是什么，或者堆栈跟踪，或者其他任何可以帮助我确定断言失败原因的东西？