From: martin@gkc.org.uk   
      
   On 18/01/2023 13:14, Spiros Bousbouras wrote:   
      
   There's no assumption that UB (undefined behaviour) will not happen, both   
   possibilities are accounted for.   
      
      
   The "assumption that UB will not happen" is shorthand for the idea   
   that any optimisation is valid if the optimised code is a refinement   
   of the unoptimised code for all initial states such that UB does not   
   occur. Equivalently, a proposed optimiation is valid if we represent   
   UB as "abort" (a statement which can be refined to anything) and the   
   optimised code is a refinement of the unoptimised code for all initial   
   states.   
      
   --   
               Martin   
      
   Dr Martin Ward | Email: martin@gkc.org.uk | http://www.gkc.org.uk   
   G.K.Chesterton site: http://www.gkc.org.uk/gkc | Erdos number: 4   
      
   --- SoupGate-Win32 v1.05   
    * Origin: you cannot sedate... all the things you hate (1:229/2)