Thanks for trying it out! I think a couple of your snippets make good examples of the difference between code and specifications, and what makes specifications particularly nasty to write.
The system is required to prevent two trains from occupying the same track segment at the same time.
newtype Track = Track [TrackSegment]
data Train = Train
data TrackSegment = SegmentTrain Train | SegmentEmpty
This type makes it impossible to have two trains in the track segment at the same time. I don’t think that’s our goal of this spec! When I see “the system is required to prevent X”, I infer two things:
X is a possible state, in that it can happen
X is an invalid state, in that it shouldn’t happen
In other words, it is possible for two trains to be on the same track segment, but our system should guarantee that, if everything follows the specification, our system will never cause two trains to overlap.
I don’t think Haskell’s type system is powerful enough to specify this, but you can probably do it in dependent types. Whether that’s the appropriate “raw material” for this specification is another question.
(Another possible issue is that the current type spec prevents anything else from being on the tracks except a train, like people. But whether that’s an issue dependents on what it is we’re specifying.)
The vending machine can prevent a coin-insertion event, but only the customer can cause it.
allowCoinInsert :: Signal (Maybe CoinInsert) -> Signal VendingMachineState -> Signal (Maybe CoinInsert)
allowCoinInsert coinInsertS stateS = runMaybeT $ do
CoinsNotBlocked <- lift stateS
MaybeT coinInsertS
We have here that the vending machine can prevent a coin-insert event, but we haven’t actually specified that only the customer can cause it. For all we know the vending machine spec is also allowed to trigger a CoinInsert.
We could add vending machine code and not have any CoinInsert functions, but that doesn’t quite work, either. Upon seeing that, all we know is that the code doesn’t have a means for the vending machine to insert a coin. But we don’t know if that’s intended functionality (perhaps for the next sprint), unplanned-but-okay if it does happen, or expressly forbidden. Similarly, we don’t know if any other parts of the system, whether the customer, a bypasser, or the snack-filler, are allowed to insert coins.
When a button is pressed, the machine should turn the lamp on within 250 milliseconds.
-- Hmm... I could use `timeout` to *check* if this happened,
-- but I don't think I could write anything that would
-- *guarentee* it always did. It's unclear what the goal of
-- the expression is.
It means that if you press the button, the light goes on within 250 milliseconds. :P
This is an example of hard real-time specification: you specify that the system must do something within a given time range. If your system takes 255 ms to flip the light, then your system is wrong. Hard time specifications are something I have zero experience in, nor have I ever used any specification languages that can express those properties.
The pipes and switches of the package routing machine form a binary tree.
data Pipe = EndPipe | Pipe Switch Switch
data Switch = EndSwitch | Switch Pipe Pipe
This is a good example of how types can be used as a specification tool, which is something I tend to dismiss too easily.
Hard time specifications are something I have zero experience in, nor have I ever used any specification languages that can express those properties.
Always happy to fix a problem like that. I did save a lot of design and verification papers on hard-real-time systems. I can try to dig up some examples for you if you want. If you did, I’m curious if you want just the general stuff or also some examples of custom stuff. They do a lot of purpose-built formalisms in that niche. I’m still not sure if that’s a good idea or not since benefits of people being on same page often outweigh benefits of new formalisms.
Very interesting, because in the average language, some can be expressed as run time checks, others as compile time checks. Getting into more dependently typed languages allows more to be expressed at compile time, but still some are quite tricky.
Noodling around in Haskell: https://github.com/singpolyma/raw-materials
Thanks for trying it out! I think a couple of your snippets make good examples of the difference between code and specifications, and what makes specifications particularly nasty to write.
This type makes it impossible to have two trains in the track segment at the same time. I don’t think that’s our goal of this spec! When I see “the system is required to prevent X”, I infer two things:
In other words, it is possible for two trains to be on the same track segment, but our system should guarantee that, if everything follows the specification, our system will never cause two trains to overlap.
I don’t think Haskell’s type system is powerful enough to specify this, but you can probably do it in dependent types. Whether that’s the appropriate “raw material” for this specification is another question.
(Another possible issue is that the current type spec prevents anything else from being on the tracks except a train, like people. But whether that’s an issue dependents on what it is we’re specifying.)
We have here that the vending machine can prevent a coin-insert event, but we haven’t actually specified that only the customer can cause it. For all we know the vending machine spec is also allowed to trigger a
CoinInsert.We could add vending machine code and not have any
CoinInsertfunctions, but that doesn’t quite work, either. Upon seeing that, all we know is that the code doesn’t have a means for the vending machine to insert a coin. But we don’t know if that’s intended functionality (perhaps for the next sprint), unplanned-but-okay if it does happen, or expressly forbidden. Similarly, we don’t know if any other parts of the system, whether the customer, a bypasser, or the snack-filler, are allowed to insert coins.It means that if you press the button, the light goes on within 250 milliseconds. :P
This is an example of hard real-time specification: you specify that the system must do something within a given time range. If your system takes 255 ms to flip the light, then your system is wrong. Hard time specifications are something I have zero experience in, nor have I ever used any specification languages that can express those properties.
This is a good example of how types can be used as a specification tool, which is something I tend to dismiss too easily.
Always happy to fix a problem like that. I did save a lot of design and verification papers on hard-real-time systems. I can try to dig up some examples for you if you want. If you did, I’m curious if you want just the general stuff or also some examples of custom stuff. They do a lot of purpose-built formalisms in that niche. I’m still not sure if that’s a good idea or not since benefits of people being on same page often outweigh benefits of new formalisms.
My Haskell is rather poor but wouldn’t this also let you make cycles? What happens if you put the same value for both
Pipes of aSwitch?From this description, I thought something like this would be valid? But how can it be expressed?
From this diagram, I’m also thinking that having two child switches for a pipe would be invalid.
Although really, I’d ask for the statement to be clarified first. There are a few other questions here.
Very interesting, because in the average language, some can be expressed as run time checks, others as compile time checks. Getting into more dependently typed languages allows more to be expressed at compile time, but still some are quite tricky.
Reminds me of the Tony Morris Tic Tac Toe game, which was surprisingly challenging, and gave me a great afternoon of fun. http://blog.tmorris.net/posts/understanding-practical-api-design-static-typing-and-functional-programming/