Re: Implicit actions & program correctness

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

On 2020-05-25 23:15, deadhacker wrote:
> On Friday, May 15, 2020 at 3:10:02 PM UTC-7, Paul Rubin wrote:
>> You might like this article (not Ada specific):
>> 
>> http://blog.tmorris.net/posts/understanding-practical-api-design-static-typing-and-functional-programming/
>
>> 
> Paul, thank you so much for the link.  It's good reading.
> 
> To me, seems that his third requirement is the tough one.  (Quoting
> it here: "If I call move on a tic-tac-toe board, but the game has
> finished, I should get a compile-time type-error. In other words,
> calling move on inappropriate game states (i.e. move doesn’t make
> sense) is disallowed by the types.")
> 
> It seems that if I have a Move subprogram that operates on a Game, it
> & produces another Game, I don't see how it could sometimes return a
> FinishedGame that can be detected at compile-time.  (It could return
> a Game that could be checked for Finished at run-time.)
> 
> 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?

Checking such things was (and is) the goal of "typestate analysis", 
https://en.wikipedia.org/wiki/Typestate_analysis.

In Ada, it could be done statically with the precondition/postcondition 
system, plus some program proof. The Move operation would have a 
precondition "not Finished (Game)", and the prover would check that the 
program flow after any call of Move always ensures this precondition 
before Move is called again. Presumably this would be done by the 
program inspecting Finished (Game) in a control-flow condition, and 
allowing flow to a new Move call only in the "not finished" case.

Making this check "at compile-time" would of course require that the 
prover is always executed in or after any compilation.

-- 
Niklas Holsti
niklas holsti tidorum fi
       .      @       .