4 ms·

AFAIK Ada's "refinement types" are essentially ranged integer types, i.e., you can define type Int is range 0 .. 100; and it will be impossible to store a

AFAIK Ada's "refinement types" are essentially ranged integer types, i.e., you can define type Int is range 0 .. 100; and it will be impossible to store any number outside that range in a variable of this type. But you can't define more general properties than this.

mcguire 9y ago
In general Ada, those are only checked at runtime, IIRC.
- junke 9y ago
  Types are checked by names, even you have the same underlying range of values. But some checks can only be done at runtime.
badsectoracula 9y ago
Pascal also has this, but i remember some Ada-related post from a few months ago here that had code along the lines of (imaginary syntax, i don't remember the exact code): type Int is range 0 .. 100 check(v) if (v = 10) or (v = 50) then error; end; That would allow all values of v between 0 and 100, except 10 and 50. Note that everything after (and including) "check" is something i came up (and is more Pascal-ish), not what i am talking about. I also remember that this could be used with objects so that you could have something like (this one is Object Pascal-ish, i do not know Ada): type Foo = object Enabled : Boolean; Magnitude : 0..1000; check if (Enabled and (Magnitude=0)) or (not Enabled and (Magnitude > 0)) then error; end; procedure Bar; end; The code in check would be called whenever the object changes externally, so "Bar" can change Enabled and Magnitude with the check being invoked only at the exit of Bar to ensure object consistency and not whenever Bar does the assignment (so it can do a Enabled:=False; Magnitude:=0; and not fail at the first assignment), but assigning those values directly from outside the object would trigger it (so having a var f: Foo; and then writing f.Enabled:=True; would trigger the error). Or at least that is what i remember understanding. Maybe i remember some other Pascal-styled language, but the only other such language i know of is Oberon and that goes against the "put everything imaginable, plus extra more" mentality of Ada seems to have :-P.
- touisteur 9y ago
  You might be thinking of type predicates, added in Ada2012 : http://sworthodoxy.blogspot.fr/2015/08/ada-2012-type-invariants-and-predicates.html http://sworthodoxy.blogspot.fr/2015/08/ada-2012-type-invaria... some of them statically provable in Spark : http://www.spark-2014.org/entries/detail/spark-2014-rationale-type-predicates http://www.spark-2014.org/entries/detail/spark-2014-rational... (if interested, there's a link down there with a 'rationale' pdf).

mcguire 9y ago

In general Ada, those are only checked at runtime, IIRC.

junke 9y ago
Types are checked by names, even you have the same underlying range of values. But some checks can only be done at runtime.

badsectoracula 9y ago

Pascal also has this, but i remember some Ada-related post from a few months ago here that had code along the lines of (imaginary syntax, i don't remember the exact code): type Int is range 0 .. 100 check(v) if (v = 10) or (v = 50) then error; end; That would allow all values of v between 0 and 100, except 10 and 50. Note that everything after (and including) "check" is something i came up (and is more Pascal-ish), not what i am talking about. I also remember that this could be used with objects so that you could have something like (this one is Object Pascal-ish, i do not know Ada): type Foo = object Enabled : Boolean; Magnitude : 0..1000; check if (Enabled and (Magnitude=0)) or (not Enabled and (Magnitude > 0)) then error; end; procedure Bar; end; The code in check would be called whenever the object changes externally, so "Bar" can change Enabled and Magnitude with the check being invoked only at the exit of Bar to ensure object consistency and not whenever Bar does the assignment (so it can do a Enabled:=False; Magnitude:=0; and not fail at the first assignment), but assigning those values directly from outside the object would trigger it (so having a var f: Foo; and then writing f.Enabled:=True; would trigger the error). Or at least that is what i remember understanding. Maybe i remember some other Pascal-styled language, but the only other such language i know of is Oberon and that goes against the "put everything imaginable, plus extra more" mentality of Ada seems to have :-P.

touisteur 9y ago
You might be thinking of type predicates, added in Ada2012 : http://sworthodoxy.blogspot.fr/2015/08/ada-2012-type-invariants-and-predicates.html http://sworthodoxy.blogspot.fr/2015/08/ada-2012-type-invaria... some of them statically provable in Spark : http://www.spark-2014.org/entries/detail/spark-2014-rationale-type-predicates http://www.spark-2014.org/entries/detail/spark-2014-rational... (if interested, there's a link down there with a 'rationale' pdf).