[trustable-software] Exploring the "Hypothesis for software to be trustable"
dan.firth at codethink.co.uk
Wed Jan 3 12:10:46 GMT 2018
On 03/01/18 09:28, Munns, Jon wrote:
> Heres our 'guidelines'.... suggest we include 'agreed'... which.. by
> inference includes 'understood'.
> * Atomic - only one statement, e.g. it should be blue, not it should
> be blue and made of plastic
This one in particular makes no sense. It's impossible to express any
implication this way. I'll resurrect the example from the SAT solver we
investigated early last year to demonstrate.
1. A box contains electrical wires that can be powered 'on' or 'off'
2. The workman can either be either in the state 'at risk' or 'safe'
3. The box door can either be open or closed
4. When the box is open and the power on, the workman is 'at risk'
5. When the box is closed, the workman is 'safe'
6. When the door is opened, the power is turned off
7. When the door is closed, the power is turned on
8. The workman should never be at risk
1,2,3 are all of the form A \/ B
4,5,6,7 are all of the form A => B, equivalently B \/ ¬A
There's no way to express any requirement with a non-trivial amount of
semantic content without allowing conjunctive/disjunctive requirements.
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the trustable-software