Re:Implications of Rewriting a Browser Component in Rust
by pjmlp on Friday March 01, 2019 @01:07AM
(#19278321)
SPARK is a subset of Ada 2012.
Your examples are possible with contracts.
Re:Implications of Rewriting a Browser Component in Rust
by Yoric on Friday March 01, 2019 @05:41AM
(#19279383)
I'm interested, do you have examples somewhere on how to implement that kind of properties with contracts?
Re:Implications of Rewriting a Browser Component in Rust
by yannickmoy on Friday March 01, 2019 @06:11AM
(#19279519)
You can look at this blog post where I used a ghost global variable to hold the current state of the game (see section "Proving Functional Properties of Tetris Code"): https://blog.adacore.com/tetris-in-spark-on-arm-cortex-m4
You can similarly express ghost properties of your types, even though we don't have ghost fields in SPARK. For more on ghost code in SPARK, you can look at this presentation last year from my colleague Claire Dross: https://www.adacore.com/uploads/products/SSAS-Presentations/...
As a more extensive example of a useful library with this kind of contracts for proof, Joffrey Huguet added rich contracts of this kind to the Ada.Text_IO standard library just two weeks ago, as part of his current internship with us. This should be in the FSF trunk in the coming weeks. For example, here are some contracts he added:
procedure Open
(File : in out File_Type;
Mode : File_Mode;
Name : String;
Form : String := "")
with
Pre => not Is_Open (File),
Post =>
Is_Open (File)
and then Ada.Text_IO.Mode (File) = Mode
and then (if Mode /= In_File
then (Line_Length (File) = 0
and then Page_Length (File) = 0)),
Global => (In_Out => File_System);
procedure Put (File : File_Type; Item : Character) with
Pre => Is_Open (File) and then Mode (File) /= In_File,
Post =>
Line_Length (File)'Old = Line_Length (File)
and Page_Length (File)'Old = Page_Length (File),
Global => (In_Out => File_System);
procedure Close (File : in out File_Type) with
Pre => Is_Open (File),
Post => not Is_Open (File),
Global => (In_Out => File_System);
1/ Consider a file `f` (or a socket, etc.). Using the standard library, Rust will statically ensure that, once the file is closed, you cannot attempt to, say, read from it. This is nothing special to files, just an aspect of the borrow checker.
2/ Consider a communication protocol. You need to send a message `HLO`, expect a message `ACK`, then send something else, etc. It is pretty easy to design your objects such that the operations of sending the message, receiving the message, etc. will change the type of your protocol object, ensuring statically that you never send/expect a message that you're not supposed to send in the current state.
If you're curious, I wrote a blurb last year on the topic: https://yoric.github.io/post/rust-typestate/
3/ I quickly googled "Ada spark phantom types" and didn't find anything. Does Ada support phantom types?