slice_postcon.adb

package body Slice_Postcon
is
   
   function Check_Proto (Data : Data_Type) return Boolean
   is
   begin
      if Data (Data'First) = 'X'
      then
         pragma Assume (Is_Proto (Data (Data'First + 1 .. Data'Last)));
         return True;
      end if;
      return False;
   end Check_Proto;

   function Use_Proto (Data : Data_Type) return Character
   is
   begin
      return Data (Data'First);
   end Use_Proto;

   function Example_OK (Data : Data_Type) return Boolean
   is
   begin
      if Check_Proto (Data)
      then
         return Use_Proto (Data (Data'First + 1 .. Data'Last)) = 'A';
      end if;
      return False;
   end Example_OK;

   function Example_Fail (Data : Data_Type) return Boolean
   is
   begin
      -- This cannot be proved as we use Data without having checked it
      -- actually contains the right protocol.
      return Use_Proto (Data (Data'First + 1 .. Data'Last)) = 'A';
   end Example_Fail;

end Slice_Postcon;

slice_postcon.ads

package Slice_Postcon
   with SPARK_Mode
is
   type Data_Type is array (Natural range <>) of Character;

   -- Check whether Data contains proto
   function Is_Proto (Data : Data_Type) return Boolean
   with
      Ghost, Import;

   function Check_Proto (Data : Data_Type) return Boolean
   with
      Pre  => Data'Length > 1 and Data'First < Natural'Last,
      Post => (if Check_Proto'Result then Is_Proto (Data (Data'First + 1 .. Data'Last)));

   function Use_Proto (Data : Data_Type) return Character
   with
      Pre => Is_Proto (Data) and Data'Length > 1;

   function Example_OK (Data : Data_Type) return Boolean
   with
      Pre  => Data'Length > 2 and Data'First < Natural'Last;

   function Example_Fail (Data : Data_Type) return Boolean
   with
      Pre  => Data'Length > 2 and Data'First < Natural'Last;

end Slice_Postcon;