Re: Implicit actions & program correctness

[Niklas Holsti <niklas.holsti@tidorum.invalid>]

On 2020-05-26 1:31, Paul Rubin wrote:
> deadhacker <gstover@gmail.com> writes:
>> Sadly, his Java API is no longer available, so I can't see how he
>> solved it.
>> Do you (or anyone else here) know how it could be solved with Ada?
> 
> I didn't look at the Java code (don't know if it was posted somewhere)
> but I'd expect it is done with Java classes and subclasses.  You'd have
> a class for game state, and container (wrapper) classes for "initial",
> "non-initial", "finished", and "non-finished".  Each wrapper would
> either be empty, or contain a state of the specified type.
> 
> The "move" function would accept a non-finished state as a parameter,
> and return three maybe-empty wrapper objects containing the new state.
> To call "move" again you'd have to look in the "non-finished" wrapper to
> get a non-finished state from it, in the event that there is one.  If
> the non-finished wrapper is empty, then the game is finished and there
> is no way to call "move" again.   Similarly with takeback, etc.

That, of course, is basically a run-time check, and not a compile-time 
check as was originally desired. But as for Ada, program-proving tools 
could be applied at compile-time to verify that the program does check 
(at run-time) if "move" can be called again.

-- 
Niklas Holsti
niklas holsti tidorum fi
       .      @       .