Re: SPARK 2014 and protected objects

[Shark8 <onewingedshark@gmail.com>]

On Wednesday, August 31, 2016 at 1:42:51 AM UTC-6, Simon Wright wrote:
> 
> We seem to have come up with (almost) the same solution, which gives me
> confidence it's the right one. Thanks.

You're quite welcome.
 
> I had Protected_Value outside the PO because it's standing in for a
> number of I/O registers communicating with devices on a shared SPI bus
> via their /Chip Select lines. Not sure how to deal with the concept of
> "a number of machine registers"!

Well, if they're memory-mapped registers you could use something like:
Regester_A : Word with Address => Location;

If they aren't, you may have to be a bit more complex. Perhaps something like:
Type Register is (AX, BX, CX, PC, Flags);
Subtype GP_Register is Register range AX..Register'Pred(PC);

-- Implemented w/ Machine_Code.
Procedure Read ( Item : GP_Register; Value : out Value_Type );
Procedure Write( Item : GP_Register; Value :  in Value_Type );