title: Is a software bug always a logical contradiction?
body: <p>While doing my studies on propositional logic i came up with the following question:</p>
  
  <p><strong>Is a software bug always a logical contradiction between the program and the specification?</strong></p>
  
  <p>Consider the following example:
  Our specification tells us that "<em>we do action C iff premise A and B are true</em>".</p>
  
  <p>Which is implemented as follows:</p>
  
  <pre><code>main ()
    if A then C
    if B then C
  </code></pre>
  
  <p>Clearly one can see that the specification does not fit the implementation since (consider the program above) "<em>we do C iff the premise A or the premise B is true</em>".</p>
  
  <p>Expressing our specification and our program as propositional formulas we get the following equation:</p>
  
  <p><a href="https://i.stack.imgur.com/3kIBm.gif" rel="nofollow noreferrer"><img src="https://i.stack.imgur.com/3kIBm.gif" alt="enter image description here"></a></p>
  
  <p>We transform our specification to CNF and apply the resolution calculus and now we can easily see that the very first clause contradicts with the very last clause. Therefore this formula is not satisfiable and therefore our specification contradicts our implementation.</p>
  
  <p>My questions are now (since the above was only an example):</p>
  
  <p><strong>Is this true for every software bug assuming a complete documentation?</strong></p>
  
  <p>and if so:</p>
  
  <p><strong>If we convert a complete specification to propositional formulas could we automate the process of software bug finding?</strong></p>