src/HOLCF/IOA/NTP/Read_me
changeset 17242 dbe74ac57236
parent 3073 88366253a09a
equal deleted inserted replaced
17241:62bb8dcc316e 17242:dbe74ac57236
     1 Isabelle Verification of a protocol using IOA.
     1 Isabelle Verification of a protocol using IOA.
     2 
       
     3 ------------------------------------------------------------------------------
       
     4 The theory structure looks like this picture:
       
     5 
       
     6      Correctness
       
     7 
       
     8         Impl
       
     9 
       
    10 Sender Receiver Channels Spec
       
    11 
       
    12  Action    IOA      Multisets
       
    13 
       
    14  Packet        List 
       
    15 
       
    16          Arith
       
    17 
     2 
    18 ------------------------------------------------------------------------------
     3 ------------------------------------------------------------------------------
    19 
     4 
    20 The System.
     5 The System.
    21 
     6