From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-1.9 required=5.0 tests=BAYES_00
	autolearn=unavailable autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!feeder.eternal-september.org!news.uzoreto.com!fu-berlin.de!uni-berlin.de!individual.net!not-for-mail
From: Niklas Holsti <niklas.holsti@tidorum.invalid>
Newsgroups: comp.lang.ada
Subject: Re: Implicit actions & program correctness
Date: Tue, 26 May 2020 11:47:36 +0300
Organization: Tidorum Ltd
Message-ID: <hj43d9F2cl7U1@mid.individual.net>
References: <d4cc5c66-b82a-4ef7-8e69-2fa9b7bd99a6@googlegroups.com>
 <r9mp29$6nd$1@dont-email.me>
 <3c545096-d000-4d09-b3fe-ad8530632457@googlegroups.com>
 <871rnk97ew.fsf@nightsong.com>
 <14afb70d-cb70-4ca2-bd24-f9d9664ee103@googlegroups.com>
 <87o8qb7ikc.fsf@nightsong.com>
Mime-Version: 1.0
Content-Type: text/plain; charset=utf-8; format=flowed
Content-Transfer-Encoding: 7bit
X-Trace: individual.net yOAFpLJhFWRPoFqARunu3AlNFM9mPh1rb9P1r/sM9vEERDALil
Cancel-Lock: sha1:GSLSDv9LghnBBG6b59Q/zZsmeSk=
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.14; rv:68.0)
 Gecko/20100101 Thunderbird/68.5.0
In-Reply-To: <87o8qb7ikc.fsf@nightsong.com>
Content-Language: en-US
Xref: reader01.eternal-september.org comp.lang.ada:58790
Date: 2020-05-26T11:47:36+03:00
List-Id: <comp.lang.ada>

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
       .      @       .