[trustable-software] Exploring the "Hypothesis for software to be trustable"

Daniel Firth dan.firth at codethink.co.uk
Wed Jan 3 16:42:06 GMT 2018



On 03/01/18 16:16, Paul Sherwood wrote:
> Hi Dan,
> On 2018-01-03 12:10, Daniel Firth wrote:
>> 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.
>
> I think I understand your point, but I confess I've never before seen 
> the notation you're using... can you provide a link to help us 
> decipher it, please? :)
>
>

here's a crib for the notation: 
https://en.wikipedia.org/wiki/Logical_connective#Common_logical_connectives

this is the wider theory: 
https://en.wikipedia.org/wiki/Boolean_satisfiability_problem

The underlying representation of the previous example in a solver would 
look something pseudo-like this:

1. A OR B
2. C OR D
3. E OR F
4. (E AND A) IMPLIES C
5. F IMPLIES D
6. E IMPLIES B
7. F IMPLIES A
8. NOT C

or in normal form, given that these 8 reqs together form a conjunctive 
set that all must be true simultaneously:

(A \/ B) /\ (C \/ D) /\ (E \/ F) /\ ((E /\ A) => C) /\ (F => D) /\ (E => 
B) /\ (F => A) /\ ¬C

SAT solvers are aimed at determining whether or not the above formula 
could ever be true, could ever be false, and in how many ways, divorced 
from their english representation. Some are quite fast on thousands of 
connected sentences (Z3)

Here's one that isn't fast that I knocked up in purescript: 
http://locallycompact.gitlab.io/SMTSandbox/

Dan



More information about the trustable-software mailing list