[SOLVED] How do i add constraints/contracts to a generic parameter?

General
1

I’m trying to learn SPARK by implementing a Euclidean Ring package. (Don’t let the mathematics scare you; it’s not really relevant.) The package is generic, with several parameters that needs specification. Among these are a Size function, a Zero function, and a rem function.

If SPARK is to have any prayer at all of proving correctness, the rem function needs a constraint along these lines:

    generic

       -- a bunch of stuff omitted

       with function "rem" ( Dividend, Divisor : Ring_Element ) return Ring_Element
          is <>
              with
                 Pre => Divisor /= Zero,
                 Post => (
                             "rem"'Result /= Zero
                          or else Size ( "rem"'Result ) < Size ( Divisor )
                         )
       ;

…and the compiler chokes on the contracts:

euclidean.ads:39:13: incorrect placement of aspect "Pre"
euclidean.ads:40:13: incorrect placement of aspect "Post"

Originally I tried placing it before the is <> but that didn’t work, either.

So… where does one specify constraints for the parameters to a generic?

2

Hi Cantanima,

I am by no means an Ada expert, forget then SPARK. However, contracts are added before the is <> part. What was the error you were getting before?

Also, you have write Divisor /= Zero and "rem"'Result /= Zero, Is Zero a function with no parameters? otherwise you would have to write Divisor /= Zero(Divisor) if you are checking wheter Divisor is “Zero” or not.

Also, I find it strange that the function "rem" is being defined inside a with. I would have expected the prototype/spec to be defined somewhere else (with contracts). I have never seen a with inside a with. But maybe I am just not knowledgeable enough :slight_smile:

Those are my two cents. Hopefully they were somewhat useful. Best,
Fer

3

When I place them before, I get this error:

euclidean.ads:45:22: missing ";"

That’s pointing to the end of the postcondition; i.e.,

            Post => (
                        "rem"'Result /= Zero
                     or else Size ( "rem"'Result ) < Size ( Divisor )
                    )
            -------^ end of the line above
      is <>
   ;

In addition, when you define a function inline, you have to define the aspects after. For example, this passes the compiler. I don’t know why, but:

       -- this compiles
       function Integer_Size ( Value : Integer ) return Integer
       is
          ( abs ( Value ) )
             with
                Pre => Value > Integer'First;

…whereas if I put the aspects before the is, I get the error:

main.adb:25:13: aspect specifications must come after parenthesized expression

So, having obtained the error above, I tried swapping them, to no avail.

No, it’s defined as:

       type Ring_Element is private;
       Zero: Ring_Element;

It’s a parameter to a generic package. Here’s a fuller listing, sans comments:

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 Integer;
   with function "rem" ( Dividend, Divisor : Ring_Element ) return Ring_Element
      is <>
         with
            Pre => Divisor /= Zero,
            Post => (
                        "rem"'Result /= Zero
                     or else Size ( "rem"'Result ) < Size ( Divisor )
                    )
   ;

package Euclidean is
-- etc.

I agree it looks odd, but I’m not sure how else to place pre- & postconditions on a generic parameter.

4

Thanks to @Max for the answer, via the Ada channel in Telegram: Basically, I need to use the -gnat2022 compiler switch and the following specification:

   with function "rem" ( Dividend, Divisor : Ring_Element ) return Ring_Element
      is <>
         with
            Pre => Divisor /= Zero,
            Post => (
                        "rem"'Result /= Zero
                     or else Size ( "rem"'Result ) < Size ( Divisor )
                    )
   ;

Compiles and runs :grin: :dark_sunglasses: :grinning: :sunglasses: :fireworks: :tada: :man_dancing:

1 Like
5

Note that GNATprove (the SPARK tool) only analyzes instances of generics, not the generics themselves. So a simpler way to analyze your code is to skip any contracts on generic parameters, since the code of each instance will call concrete subprograms which should have a contract (explicit, or implicit for an expression function).

But indeed, you can make GNATprove also check that your generic actuals in an instance satisfy the contract you put on the generic parameters, and that these are sufficient to prove the properties you care about. But that’s still done instance by instance.

6

Thank you for the reply. Analyzing instances of generics; I want the contract to be stated explicitly, if possible.