16 ms·

Oh wow, even with support for static type-checking. It really makes me want to give ruby another shot. Piggybacking on this: apart from F*, does someone know o

by metafex 10y ago

Oh wow, even with support for static type-checking. It really makes me want to give ruby another shot. Piggybacking on this: apart from F*, does someone know of a language or support for existing ones for contracts, loop-invariants and possibly verification? Dafny and Spec# aren't very general-purpose and apart from those nothing much comes to my mind.

losvedir 10y ago
When I think of contracts, I think of Eiffel. Not really sure how much it's actually used, though. Also, maybe Ada? I always wonder why Ada doesn't get any love on HN.
- pjmlp 10y ago
  Given that the company is still around, I would say that they manage to have a set of customers that value the language and what it offers in terms of quality.
david-given 10y ago
Ada has robust preconditions and postconditions. Untested code follows: procedure swap(a: in out integer, b: in out integer) with pre => a <> b -- just for example purposes post => (a == b'old) and (b == a'old) is declare t: integer; begin t := a; a := b; b := t; end (Sorry, couldn't think of a sensible small example which uses both pre and post, hence the terrible precondition.) Note that the postcondition can refer to the old values of the variables with the 'old suffix --- the values will be automatically saved on entry to the function and used for comparison later. Unfortunately the pre- and postconditions have to be specified in the public part of the module, so can't see any private module variables, which forces you to jump through hoops if you don't want to expose your module's internal state (e.g. checking to make sure that functions on a state machine are called in the right order). You also get type invariants, where you can specify an expression which must always be true for a number: subtype Even is integer with dynamic_predicate => (Even mod 2) == 0; Or, if you really want your mind blown: subtype Even is integer with dynamic_predicate => (for some N in integer => (Even == N*2)); There's also a static_predicate form which only supports a restricted predicate expression but which can be checked at compile time.
- metafex 10y ago
  Thank you for the example. Also: SPARK is another one I forgot. I guess I'll have to think of a nice example and just implement it in a Ada, F* and with RDL to get a hang of the differences and features.

by metafex 10y ago

losvedir 10y ago

When I think of contracts, I think of Eiffel. Not really sure how much it's actually used, though. Also, maybe Ada? I always wonder why Ada doesn't get any love on HN.

pjmlp 10y ago
Given that the company is still around, I would say that they manage to have a set of customers that value the language and what it offers in terms of quality.

david-given 10y ago

Ada has robust preconditions and postconditions. Untested code follows: procedure swap(a: in out integer, b: in out integer) with pre => a <> b -- just for example purposes post => (a == b'old) and (b == a'old) is declare t: integer; begin t := a; a := b; b := t; end (Sorry, couldn't think of a sensible small example which uses both pre and post, hence the terrible precondition.) Note that the postcondition can refer to the old values of the variables with the 'old suffix --- the values will be automatically saved on entry to the function and used for comparison later. Unfortunately the pre- and postconditions have to be specified in the public part of the module, so can't see any private module variables, which forces you to jump through hoops if you don't want to expose your module's internal state (e.g. checking to make sure that functions on a state machine are called in the right order). You also get type invariants, where you can specify an expression which must always be true for a number: subtype Even is integer with dynamic_predicate => (Even mod 2) == 0; Or, if you really want your mind blown: subtype Even is integer with dynamic_predicate => (for some N in integer => (Even == N*2)); There's also a static_predicate form which only supports a restricted predicate expression but which can be checked at compile time.

metafex 10y ago
Thank you for the example. Also: SPARK is another one I forgot. I guess I'll have to think of a nice example and just implement it in a Ada, F* and with RDL to get a hang of the differences and features.