The Case for SPARK Evolution - an April First Parable

by Yannick Moy – Apr 01, 2023

SPARK has had for a long time a possibility to partition the functional contract of a subprogram into a set of disjoint and complete cases, introduced by the aspect Contract_Cases. So you can write a contract as follows to specify the result of breeding in the game Animal Crossing:

procedure Breeding (Male, Female : Species; Offspring : out Species)
with
   Contract_Cases =>
      (Male = Female                                                                => Offspring = Female,
       Male in Pig | Squirrel and Female in Pig | Squirrel and Male /= Female       => Offspring = Hamster,
       Male in Beaver | Tortoise and Female in Beaver | Tortoise and Male /= Female => Offspring = Axolotl,
       others => True); -- nothing interesting here

But until recently, you could not specify cases that lead to an exception. This is being finalized currently by implementing support for the aspect Exceptional_Cases as defined in RFC#87. So you can rule out the absurd cases in your breeding program:

procedure Breeding (Male, Female : Species; Offspring : out Species)
with
   Exceptional_Cases =>
      (Size_Mismatch    => Size (Male) < Size (Female) / 10 or Size (Male) > 10 * Size (Female),
       Male_Eats_Female => Male in Carnivore and Female in Herbivore,
       Female_Eats_Male => Male in Herbivore and Female in Carnivore);

So, does that exhaust all the possibilities of rich specifications? We think that not, and that many other cases deserve consideration:

- rare cases like the breeding of an alligator and an ostrich - introduced by aspect Corner_Cases

- long forgotten cases like extinct species - think the dodo and soon every mammal except pets and farm animals - introduced by the aspect Cold_Cases

- "thinking out of the box" cases like the classy species with a distinctive appearance including spots and stripes - introduced by the aspect Suit_Cases

- low-profile and high-profile cases, the former like rodents, the latter like birds of prey - introduced by the aspect Lower_Cases and Upper_Cases

Watch the RFC website for an encompassing proposal soon, and let us know what you think by voting in the comments for your favorite case, from 🥚 (not very interested) to 🥚🥚🥚🥚🥚 (super excited!!!).

Don't hold your breath though. It wouldn't be the first case of a language evolution proposal made on April First that was not taken seriously.

Posted in #SPARK #Dad Jokes

About Yannick Moy

Yannick Moy is Head of the Static Analysis Unit at AdaCore. Yannick contributes to the development of SPARK, a software source code analyzer aiming at verifying safety/security properties of programs. He frequently talks about SPARK in articles, conferences, classes and blogs (in particular blog.adacore.com). Yannick previously worked on source code analyzers for PolySpace (now The MathWorks) and at Université Paris-Sud.