Add source for subprogram contracts lab

Author: frank-at-adacore

courses/spark_essentials/080_subprogram_contracts/lab/subprogram_contracts/answer/config.adc

@@ -0,0 +1 @@
+pragma SPARK_Mode (On);

courses/spark_essentials/080_subprogram_contracts/lab/subprogram_contracts/answer/lab.gpr

@@ -0,0 +1,17 @@
+project Lab is
+
+   for Object_Dir use "obj";
+
+   package Compiler is
+      for Default_Switches ("Ada") use ("-g", "-O0", "-gnato13", "-gnata", "-gnatyr", "-gnatwa");
+   end Compiler;
+
+   package Builder is
+      for Global_Configuration_Pragmas use "config.adc";
+   end Builder;
+
+   package Prove is
+      for Proof_Switches ("Ada") use ("-j0");
+   end Prove;
+
+end Lab;

courses/spark_essentials/080_subprogram_contracts/lab/subprogram_contracts/answer/math.adb

@@ -0,0 +1,60 @@
+with Ada.Characters.Handling; use Ada.Characters.Handling;
+with Ada.Text_IO;
+
+package body Math with
+  SPARK_Mode
+is
+
+   package IO is new Ada.Text_IO.Integer_IO (Integer);
+
+   function Saturated_Add
+     (X, Y : Integer)
+      return Integer is
+   begin
+      if X < 0 and Y < 0 then -- both negative
+         if X < Integer'First - Y then
+            return Integer'First;
+         else
+            return X + Y;
+         end if;
+
+      elsif X > 0 and Y > 0 then -- both positive
+         if X > Integer'Last - Y then
+            return Integer'Last;
+         else
+            return X + Y;
+         end if;
+
+      else -- one positive or null, one negative or null, adding them is safe
+         return X + Y;
+      end if;
+   end Saturated_Add;
+
+   procedure Add
+     (X, Y :     Integer;
+      Z    : out Integer) is
+   begin
+      Z := Saturated_Add (X, Y);
+   end Add;
+
+   procedure Convert
+     (S     :     String;
+      Value : out Integer) is
+      Unused : Positive;
+   begin
+      if
+        (for some C of S =>
+           not
+           (Is_Digit (C) or C = 'E' or C = 'e' or C = '+' or C = '-' or
+            C = '_'))
+      then
+         raise Invalid_String;
+      else
+         IO.Get (S, Value, Unused);
+      end if;
+   exception
+      when Ada.Text_IO.Data_Error =>
+         raise Constraint_Error;
+   end Convert;
+
+end Math;

courses/spark_essentials/080_subprogram_contracts/lab/subprogram_contracts/answer/math.ads

@@ -0,0 +1,26 @@
+package Math with
+  SPARK_Mode
+is
+
+   Invalid_String : exception;
+
+   function Saturated_Add
+     (X, Y : Integer)
+      return Integer with
+     SPARK_Mode,
+     Contract_Cases =>
+      ((X + Y in Integer)    => Saturated_Add'Result = X + Y,
+       X + Y < Integer'First => Saturated_Add'Result = Integer'First,
+       X + Y > Integer'Last  => Saturated_Add'Result = Integer'Last);
+
+   procedure Add
+     (X, Y :     Integer;
+      Z    : out Integer) with
+     Post => Z = Integer'First or Z = Integer'Last or Z = X + Y;
+
+   procedure Convert
+     (S     :     String;
+      Value : out Integer) with
+     Exceptional_Cases => (Invalid_String | Constraint_Error => True);
+
+end Math;

courses/spark_essentials/080_subprogram_contracts/lab/subprogram_contracts/prompt/config.adc

@@ -0,0 +1 @@
+pragma SPARK_Mode (On);

courses/spark_essentials/080_subprogram_contracts/lab/subprogram_contracts/prompt/lab.gpr

@@ -0,0 +1,17 @@
+project Lab is
+
+   for Object_Dir use "obj";
+
+   package Compiler is
+      for Default_Switches ("Ada") use ("-g", "-O0", "-gnato13", "-gnata", "-gnatyr", "-gnatwa");
+   end Compiler;
+
+   package Builder is
+      for Global_Configuration_Pragmas use "config.adc";
+   end Builder;
+
+   package Prove is
+      for Proof_Switches ("Ada") use ("-j0");
+   end Prove;
+
+end Lab;

courses/spark_essentials/080_subprogram_contracts/lab/subprogram_contracts/prompt/math.adb

@@ -0,0 +1,60 @@
+with Ada.Characters.Handling; use Ada.Characters.Handling;
+with Ada.Text_IO;
+
+package body Math with
+  SPARK_Mode
+is
+
+   package IO is new Ada.Text_IO.Integer_IO (Integer);
+
+   function Saturated_Add
+     (X, Y : Integer)
+      return Integer is
+   begin
+      if X < 0 and Y < 0 then -- both negative
+         if X < Integer'First - Y then
+            return Integer'First;
+         else
+            return X + Y;
+         end if;
+
+      elsif X > 0 and Y > 0 then -- both positive
+         if X > Integer'Last - Y then
+            return Integer'Last;
+         else
+            return X + Y;
+         end if;
+
+      else -- one positive or null, one negative or null, adding them is safe
+         return X + Y;
+      end if;
+   end Saturated_Add;
+
+   procedure Add
+     (X, Y :     Integer;
+      Z    : out Integer) is
+   begin
+      Z := Saturated_Add (X, Y);
+   end Add;
+
+   procedure Convert
+     (S     :     String;
+      Value : out Integer) is
+      Unused : Positive;
+   begin
+      if
+        (for some C of S =>
+           not
+           (Is_Digit (C) or C = 'E' or C = 'e' or C = '+' or C = '-' or
+            C = '_'))
+      then
+         raise Invalid_String;
+      else
+         IO.Get (S, Value, Unused);
+      end if;
+   exception
+      when Ada.Text_IO.Data_Error =>
+         raise Constraint_Error;
+   end Convert;
+
+end Math;

courses/spark_essentials/080_subprogram_contracts/lab/subprogram_contracts/prompt/math.ads

@@ -0,0 +1,20 @@
+package Math with
+  SPARK_Mode
+is
+
+   Invalid_String : exception;
+
+   function Saturated_Add
+     (X, Y : Integer)
+      return Integer;
+
+   procedure Add
+     (X, Y :     Integer;
+      Z    : out Integer) with
+     Post => Z = Integer'First or Z = Integer'Last or Z = X + Y;
+
+   procedure Convert
+     (S     :     String;
+      Value : out Integer);
+
+end Math;