[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