A Case for Properties: Programming Language Design

Re:A Case for Properties: Programming Language Design by MaxBarraclough on Sunday November 15, 2020 @04:35PM (#25105115)

Good point, Ada's runtime range checks mean that an assignment can raise an exception. [0] Part of what SPARK Ada does is to prove the absence of such constraint errors. [1]

I don't think Ada supports arbitrary user-specified constraints, but I'm no expert.

[0] https://gcc.gnu.org/onlinedocs/gcc-10.2.0/gnat_ugn/Run-Time-...

[1] https://docs.adacore.com/spark2014-docs/html/ug/en/usage_sce...

[ Parent | on HN ]

Re:A Case for Properties: Programming Language Design by haetze on Monday November 16, 2020 @05:00AM (#25110005)

You are right that SPARK tries to prove the absence of these errors. In that case you don't need these checks and turn them off. If you don't they are still run.

Ada has Dynamic_Predicate(s) which "can be any Boolean expression". [0] So, I'm guessing, you can write a pointless Predicate which does not terminate in some cases or takes unreasonably long.

[0] http://www.ada-auth.org/standards/12rat/html/Rat12-2-5.html

[ Parent | on HN ]

Re:A Case for Properties: Programming Language Design by MaxBarraclough on Monday November 16, 2020 @12:40PM (#25114568)

Thanks, I wasn't aware of that feature, I think you're right.

> In the case of Dynamic_Predicate, the expression can be any Boolean expression.

Ada functions are permitted to have side-effects (although this is disallowed in SPARK), so I imagine it would be possible to make a real mess if you wanted to.

[ Parent | on HN ]