Season’s greetings from the organizers of the 28th Ada-Europe International Conference on Reliable Software Technologies (AEiC 2024), to be held 11-14 June 2024, in Barcelona, Spain!

Accepted Journal Track papers will be published in the conference’s Special Issue of the Journal of Systems Architecture (JSA). Note that the Ada-Europe organization will waive the Open Access fees for the first four accepted papers, which do not already enjoy OA from other agreements with the Publisher.

www.ada-europe.org/conference2024/cfp.html#cfpjournal

#AEiC2024 #AdaEurope #AdaProgramming

1 post - 1 participant

Read full topic

just kidding. but this one took me a long time. We seem to have entered the fiendishly difficult phase. Fortunately, difficult problems are usually followed by not-so-difficult ones. Usually.

• I first completed part 1 using a recursive algorithm that pruned failing branches. No problem, though it was a bit slow, so I knew what was coming next.
• Yup, Part 2 inflates the input to an insane size. The first record completed quickly, to my surprise but I quit the program after it dawdled on the second record for several minutes.
• I stared at it a while.
• Finally, I visited the Reddit solutions page. People were mentioning spoiler. What the heck is spoiler, thinks I, feeling a little humiliated at not knowing. Scrolling down a little, I see that someone else has the wherewithal to ask. It means spoiler. Oh yeah, says I, albeit a little more colorfully. (i.e., ) I remember something about that from my Algorithms class. But… how?
• Reading a bit more, I see what people say they are doing. Unfortunately, they are writing in languages like C++, D, Python, Rust. Excerpts range from illegible to incomprehensible out of their context. Probably doesn’t help that’s it’s 2am. Oooookayyyyy… time for a nap.

Thinking about it this evening, I realized that I could do the following.

1. For each line, iterate over the contiguous groups from left to right. So, start with the leftmost.
2. Assume the group records n damaged springs,
   • Determine spoiler.
   • For each i in 0 … spoiler A picture is probably worth 1000 words here: if n is 3, and spoiler, look at spoiler It is easy to tell whether this matches .#?#?.***
   • If it matches, take the next contiguous group and recurse (step 2) with an appropriate starting index for the next string. (Have I mentioned how I Ada’s custom indexing?.)
   • This is a key point. If you don’t want to wait forever, spoiler

A couple of additional complications I encountered:

• The result in part 2 is larger than Natural'Last on my input, so you’ll likely need something larger.
• If you use a hashed map for the spoiler, be prepared for some moding. I do wonder if I’d have done better with an ordered map.

There was more, but I can’t remember it now.

***I don’t recall reading this detail anywhere in the Reddit discussion of solutions, but then again, I don’t think so well at 2am. Either way, I’m pleased as punch that it seemed different.

3 posts - 2 participants

Read full topic

2023/12/10:
Birthday of Lady Ada Lovelace, born in 1815.
Happy Programmers’ Day!
#AdaProgramming #AdaBelgium

3 posts - 3 participants

Read full topic

The 28th Ada-Europe International Conference on Reliable Software Technologies (AEiC 2024) will take place in Barcelona, Spain from 11 to 14 June, and comprises different tracks and co-located events.

Submission deadlines: 15 January for journal track papers; 26 February for industrial track and work-in-progress track papers, tutorial and workshop proposals. Submit early: tutorial/workshop proposals will be evaluated ASAP, with decisions from 1 January 2024!

More information on the conference site, including an extensive list of topics, and details on the call for contributions for the various tracks.

www.ada-europe.org/conference2024

#AEiC2024 #AdaEurope #AdaProgramming

1 post - 1 participant

Read full topic

When gnatprove is used with “–counterexamples=on” inside GNAT Studio it is able to present a detailed trace[1]:

This nice trace only seems to work inside GNAT Studio, not inside the VSCode AdaCore.ada plugin. Is there a way to output this trace to a text console (e.g. by passing an option to the gnatprove command-line command) so that this trace feature can be used outside GNAT Studio?

[1] 7.2. How to View GNATprove Output — SPARK User's Guide 25.0w

2 posts - 2 participants

Read full topic

A full implementation of the parallel features of Ada 2022 is yet to be released. In the meantime, here is a light-weight-threading library that provides essentially all of the parallel features of Ada 2022, using various generics, etc. Scheduling is provided using a plug-in architecture. If no scheduler is plugged in, the light-weight threads are simply executed sequentially. If a light-weight-thread scheduler is plugged in, then the light-weight threads spawned by instances of the various generic packages are managed by that scheduler.

There are currently two LWT scheduler plug-ins:

• a wrapper for the GNU implementation of OpenMP (lwt-openmp.ads)
• a work-stealing based plug-in, written entirely in Ada (lwt-work_stealing.ads)

Below is a link to the “readme.md” documentation for the GitHub lwt library. It is currently part of the ParaSail GitHub repository, but the files in “lwt” are actually independent of ParaSail. ParaSail has its own work-stealing-based scheduler built-in, but at some point we plan to shift over to using the “lwt” library. But at the moment, there is no dependence either way between the ParaSail interpreter/compiler and the lwt library.

Feel free to open GitHub Issues if you find problems with the implementation, or have suggestions for improvements.

Enjoy!

-Tucker Taft

The ParaSail GitHub repository was created by my colleague Olivier Henley, and he has also helped to improve the documentation and testing scripts. Much appreciated!

2 posts - 2 participants

Read full topic

GNATCOLL.Refcount provides a procedure to run some code when the reference-counted element is released.

How do I implement this procedure?

I’m clearly missing something because Release is not visible as GNATCOLL.Refcount.Release and this doesn’t work

type Context_Contents is new GNATCOLL.Refcount.Refcounted with record
    Address : System.Address;
end record;

procedure Release is new GNATCOLL.Refcount.Release
   (Self => Context_Contents);

and gives me

usb.ads:29:47: error: "Release" not declared in "Refcount"

4 posts - 3 participants

Read full topic

The 28th Ada-Europe International Conference on Reliable Software Technologies (AEiC 2024) will take place in Barcelona, Spain in the week of 11-14 June.

The conference schedule comprises a journal track, an industrial track, a work-in-progress track, a vendor exhibition, parallel tutorials, and satellite workshops.

Deadlines: 15 January 2024 for journal-track papers; 26 February 2024 for industrial-track and work-in-progress-track papers, tutorial and workshop proposals.

More information is available on the conference site, including an extensive list of topics; details on the call for contributions for the various tracks will follow shortly.

www.ada-europe.org/conference2024

#AEiC2024 #AdaEurope #AdaProgramming

1 post - 1 participant

Read full topic

@PTC continues their regular releases of their #AdaProgramming language toolsets #PTCObjectAda and #PTCApexAda Companies PTC - Ada Resource Association

1 post - 1 participant

Read full topic

To help learn me some SPARK, I decided to try implementing the Euclidean Algorithm. With a generic type. Basically (simplified from what I actually have, which includes contracts):

generic

   type Ring_Element is private;

   Zero : Ring_Element;

   with function "=" (Left, Right : Ring_Element) return Boolean is <>;
   with function Size (Value : Ring_Element) return Natural;
   with function "-" ( Left, Right : Ring_Element ) return Ring_Element is <>;
   with function "rem"
     (Dividend, Divisor : Ring_Element) return Ring_Element is <>;
package Euclidean is ...

And the body Euclidean:

    function Gcd ( A, B : Ring_Element ) return Ring_Element is

       M: Ring_Element := A;
       N: Ring_Element := B;

    begin

       while N /= Zero loop

          declare
             R : constant Ring_Element := M rem N;
          begin
             M := N;
             N := R;
          end;

       end loop;

    end Gcd;

The algorithm has several nice properties. One is a loop invariant that r divides a - b.

I’ve struggled with getting SPARK to accept a contract to that effect. My latest iteration has this:

   if R /= Zero then ( A rem R ) - ( B rem R ) = Zero

…but when I instantiate Ring_Element => Integer it reports

   euclidean.adb:26:41: medium: loop invariant might fail in first iteration, cannot prove (A rem R ) - ( B rem R ) = Zero, in instantiation at main.adb:32 (e.g. when A = -2 and B = 1 and M = 1 and R = 3)[#0]

That… makes no sense. It’s not possible for the algorithm to start with those inputs and end up with R = 3.

1. Am I misreading the error report?
2. How does SPARK come up with this value of R?
3. Any advice on writing a contract for this condition? I’ve generally had trouble with guaranteeing arithmetic expressions like A + B and A - B; I understand why, but am not sure how to handle them. Using rem R was something I thought might help here, it did get me past the under/overflow, and it is also true.

10 posts - 3 participants

Read full topic

Hi all,

We finally have GNAT FSF 13 builds available in Alire, in a separate branch for now. To try it, add an index like so:

alr index "--add=git+https://github.com/alire-project/alire-index#gnat-fsf-13.1.0" --name=gnat_fsf_13 --before=community

Apologies for the delay, this release was particularly difficult to build for no good reasons (GitHub CI, time available, etc.). Also note that the compilers hosted on macOS x86_64 are missing, I will try to make them available ASAP.

1 post - 1 participant

Read full topic

Introducing Cashe: a Money library written in Ada!

There’s quite a bit of examples in the readme, but I also gave full code examples for almost all of the functions in the API Documentation.

The purpose of Cashe is to give Money its own high-precision datatype taking advantage of Ada’s fixed type decimal system. This allows storing money, associated with a currency, at a defined precision with the choice of utilizing fuzzy or exact equality (see readme for more details).

It supports Ada-ISO Currencies as well as Custom-defined currencies, and even a working Currency Exchange.

While this is technically in pre-release, it’s passing all of my unit tests and I’m working on getting the version 1.0 out and into Alire soon.

1 post - 1 participant

Read full topic

Main URL: https://hacadacompiler.sourceforge.io/
Sources, site #1: HAC Ada Compiler download | SourceForge.net
Sources, site #2: GitHub - zertovitch/hac: HAC Ada Compiler - a small, quick Ada compiler fully in Ada
Alire Crate: Alire - Hac

What’s new:

• You can use a loop’s name for the exit statement: exit Loop_Name.
• You can exit multiple, nested, loops, by using exit Loop_Name.
• Ada semantics are better verified:
  • Array indexing (i)(j) (array of array) and (i,j) (multi-dimensional array) are no more treated as equivalent (this feature was a remnant of the Pascal syntax).
  • Separation between Type and Subtype declarations (anonymous types are allowed only in the few cases foreseen by the language).
  • Operators of the HAT package (+, -, &) are visible without prefix only in the scope of a use HAT; clause.

Note that correct Ada programs, in relation to the above points, were already accepted and parsed correctly by HAC before that change.

Finally, a bit of cosmetics in the build messages:

C:\Ada\hac\exm>..\hac -v2 -c pkg_demo.adb

*******[ HAC ]*******   HAC is free and open-source. Type "hac" for license.
       [ HAC ]          HAC Ada Compiler version 0.26, 08-Jul-2023
       [ HAC ]          Compiling main: pkg_demo.adb
       [ HAC ]          | Compiling x_pkg_demo_s.ads (specification)
       [ HAC ]           \ Compiling x_pkg_demo_s1.ads (specification)
       [ HAC ]            \ Compiling x_pkg_demo_s11.ads (specification)
       [ HAC ]            /           x_pkg_demo_s11.ads: done.
       [ HAC ]            \ Compiling x_pkg_demo_s12.ads (specification)
       [ HAC ]            /           x_pkg_demo_s12.ads: done.
       [ HAC ]            \ Compiling x_pkg_demo_s13.ads (specification)
       [ HAC ]            /           x_pkg_demo_s13.ads: done.
       [ HAC ]           /           x_pkg_demo_s1.ads: done.
       [ HAC ]           \ Compiling x_pkg_demo_s2.ads (specification)
       [ HAC ]            \ Compiling x_pkg_demo_s21.ads (specification)
       [ HAC ]            /           x_pkg_demo_s21.ads: done.
       [ HAC ]            \ Compiling x_pkg_demo_s22.ads (specification)
       [ HAC ]            /           x_pkg_demo_s22.ads: done.
       [ HAC ]            \ Compiling x_pkg_demo_s23.ads (specification)
       [ HAC ]            /           x_pkg_demo_s23.ads: done.
       [ HAC ]           /           x_pkg_demo_s2.ads: done.
       [ HAC ]           \ Compiling x_pkg_demo_s3.ads (specification)
       [ HAC ]            \ Compiling x_pkg_demo_s31.ads (specification)
       [ HAC ]            /           x_pkg_demo_s31.ads: done.
       [ HAC ]            \ Compiling x_pkg_demo_s32.ads (specification)
       [ HAC ]            /           x_pkg_demo_s32.ads: done.
       [ HAC ]            \ Compiling x_pkg_demo_s33.ads (specification)
       [ HAC ]            /           x_pkg_demo_s33.ads: done.
       [ HAC ]           /           x_pkg_demo_s3.ads: done.
       [ HAC ]          |           x_pkg_demo_s.ads: done.
       [ HAC ]          | Compiling x_pkg_demo_m.ads (specification)
       [ HAC ]          |           x_pkg_demo_m.ads: done.
       [ HAC ]          | Compiling x_pkg_demo_b.ads (specification)
       [ HAC ]          |           x_pkg_demo_b.ads: done.
       [ HAC ]          Compilation of pkg_demo.adb (main) completed
       [ HAC ]          ------  Compilation of eventual with'ed unit's bodies  ------
       [ HAC ]          | Compiling x_pkg_demo_s.adb (body)
       [ HAC ]          |           x_pkg_demo_s.adb: done.
       [ HAC ]          | Compiling x_pkg_demo_s1.adb (body)

6 posts - 3 participants

Read full topic

I’m working on a system in SPARK and am confused by a warning SPARK is giving about data races.

I’m working on a message passing system that manages several endpoints. There are multiple types of messages. Each message is a record with a Message_Type component specifying the type of the message. To use the system, endpoints use a register procedure and declare what message types they’re allowed to receive.

The system tracks what types of messages can be received by each endpoint in an abstract package state Metadata with Ghost belonging to the message system package. The Send_Message procedure then has preconditions that check with the message system to verify that the receiving endpoint has declared it can receive the type of message being sent.

All the endpoints are initialized at the start of the program by a single thread. Later in the program they’re used by different threads. These later threads will never need to alter Metadata. They take it as a Proof_In global variable.

SPARK is saying that there is a data race possible because the multiple threads are using the Metadata state.

cubedos-time_server-messages.adb:85:09: high: possible data race when accessing variable “message_manager.mailbox_metadata”[#2]
cubedos-time_server-messages.adb:85:09: high: task “cubedos.time_server.messages.send_tick_messages” accesses “message_manager.mailbox_metadata”[#3]
cubedos-time_server-messages.adb:85:09: high: task “cubedos.time_server.messages.message_loop” accesses “message_manager.mailbox_metadata”[#4]

How is this possible? If Metadata is Ghost, shouldn’t it never actually be evaluated at runtime?

Suppose that Metadata wasn’t Ghost. Is there a way I can communicate to SPARK that Metadata should be immutable after all the endpoints are initialized?

Thank you.
Any light

4 posts - 3 participants

Read full topic

Lisbon, Portugal, June 14, 2023. Ada-Europe today announced, at
its 27th International Conference on Reliable Software Technologies
(AEiC 2023), that the Ada 2022 Language Reference Manual (LRM) will
be published by Springer in its LNCS series later this year.

Ada 2022 is the latest edition of the Ada programming language
standard, technically denominated ISO/IEC 8652:2023, which was
formally approved and officially published by ISO, the Geneva-based
International Organization for Standardization, on May 2, 2023.

The Ada 2022 LRM is available online:
Ada 2022 Language Reference Manual.
An overview of Ada 2022 is at:
Ada 2022 Overview.

To mark this official milestone, and in continuation of its established
practice, Ada-Europe undertook to support the production of the new
LRM as a dedicated issue of the Springer-published LNCS series.

www.ada-europe.org/press/20230614-Ada2022-Springer.pdf

#Ada2022 #AdaEurope #AdaProgramming

5 posts - 3 participants

Read full topic

Tue 13 - Fri 16 June 2023

Final call: check out rich conference, tutorial, and workshop program!
Final Program available on conference web site.
Interested in Ada or reliable software? See you in Lisbon, Portugal!

For all information: Ada-Europe 2023, and our Usenet newsgroup postings for an overview.

#AEiC2023 #AdaEurope #AdaProgramming

1 post - 1 participant

Read full topic

LEA is a Lightweight Editor for Ada

Web site: http://l-e-a.sf.net/
Source repository #1: LEA / Code / [r343]
Source repository #2: GitHub - zertovitch/lea: LEA is a Lightweight Editor for Ada

Recent changes:

• Added auto insert feature: e.g. typing ( inserts ).
• Added color theme Solarized Light.
• Added a “stealth mode” in which LEA doesn’t leave
  traces in the registry.
• Editor adds -- if the cursor is within a comment when the Return key
  is pressed (consequence: a comment is split into two comments).
• If the cursor is within a string literal when the Return key is
  pressed, the string literal is split into two valid string
  literals with a & between them.
• Added unhandled exception information to message list
• Tabs with the various file names
• LEA doesn’t write scilexer.dll as a file; thus, it runs as
  a portable application (in the sense: you can run it from a
  read-only drive directly, without installation)
• Added a Build & Run button (for the HAC compiler).

Features:

• multi-document
• multiple undo’s & redo’s
• multi-line & multi-point edit, rectangular selections
• color themes, easy to switch
• duplication of lines and selections
• syntax highlighting
• parenthesis matching
• bookmarks

Currently available on Windows.
Gtk or other implementations are possible: the LEA_Common[.*] packages
are pure Ada, as well as HAC.

Enjoy!

3 posts - 2 participants

Read full topic

Dear all,

this forum post was already written to the C.L.A, but I think it is worthy of being here too, as it may reach even more people. So here goes a summary of what I wrote over at the C.L.A.

What and Why? Ada monthly meetup

I would like to have a monthly meetup to gather the community, see each other, talk about some things and let people present or showcase their work and discuss the news.

When and how?

It would take place once a month and it should last between 45 min to 1 h. This would allow the discussion or showcase of two or three topics and leave room for discussion and smaller news.

The meetup would take place (initially) over Jitsi, a libre conferencing software that does not require installation (it uses modern web browsers for the clients). This would be the initial platform to test the waters and see if it works well for us.

I have selected Saturday 3, June 2023 to be the day we start. It would take place the first weekend of each month with the exception of August (as it is summer in most places, maybe even September) and February, as FOSDEM takes place.

The time would be around 12:00 or 13:00 UTC. That should be a more or less approachable time for most people all over the globe. Though I am aware that it is not great for those in the Americas or in eastern Asia/Australia. It is also meal time in EU, but that is a compromise for everyone. And of course, this is just the first proposal. We will keep improving things as we move along.

How to participate?

You can join just to listen and chat! That is probably what I will end up doing most. However, there are a few things we are looking for:

• Tool developers that would like to showcase its features or new releases.
• Demos of projects.
• Issues within the language or technical problems with tools.
• Cool stuff!
• Questions!

This is a community oriented meetup, not a super heavy technical one, we leave those to the ARG

Feedback

There has already been some feedback over at the C.L.A., but some more would surely help. If you have any questions, issues or recommendations, please, share those!

Best regards,
Fer

16 posts - 6 participants

Read full topic

http://www.ada-europe.org/conference2023/

The 27th Ada-Europe International Conference on Reliable Software Technologies (AEiC 2023) returns to Portugal after 5 years, to take place in Lisbon, in the week of 13-16 June.

The conference program includes two core days with various presentations, bracketed by one day with 6 tutorials, and one day with 2 satellite events. There will be time for networking during breaks as well as social events around historic, cultural, scenic, and culinary highlights of Lisbon.

For more info and latest updates see the conference web site. You’ll find there an overview of the program, the list of accepted papers and presentations, and descriptions of workshops, tutorials, keynote presentation and panel, and social events. Also check the conference site for registration, accommodation and travel information.

Online registration is open. Reduced fees for various groups. Early registration discount until 22 May.

#AEiC2023 #AdaEurope #AdaProgramming

2 posts - 1 participant

Read full topic