Known Issues for KeY 1.2.0
==========================
 
1) "for" and "do-while" loops

     Description: 

       There is currently no invariant rule for "for" or "do-while"
       loops.
     
     Workaround: 

       Use induction or rewrite these loops as "while" loops.

     Plan: 

       Loop invariant rules will be added for this kind of loops.

2) No support for "recursions" 
    
    Description: 

    Recursive methods cannot be proven.

    Workaround: n/a

    Plan: 

      Proof obligations for recursive methods will be released in one
      of the next technical preview versions.

3) Proof cannot be loaded

   Description: 

     Loading of a proof fails.

   Workaround: 

     First make sure that you haven't changed anything in your
     implementation or specification. If this is not the case, there
     are some situations where saving and loading of proofs fails, but
     in most cases the saved proof can be recovered by manual
     editing. Please ask the KeY team for support.

4) Variable renaming confusing

   Description: 

     Introduction of new variable names and renaming lack transparency.
   
   Explanation: 

     When introducing new program variables the chosen names have to
     be unique. In order to guarantee this, names of the kind
     "basename#number" are introduced. When the declaration of such a
     new variable is removed by symbolic execution, renaming takes
     place in order to get rid of the hash symbol.
   
   Plan: 

     The process of renaming is sound thus it is not a real bug, but
     this kind of implicit renaming may confuse the user. We need to
     collect more experience.
     
5) Autoscrolling for drag and drop does not work well for
   Linux/Solaris.
   
   Explanation: 

     This is a bug of the JDK implementation. A found workaround would
     cause KeY to run only on JDK 1.5 or above. Thus it is not
     included yet.

76 Method contracts can lead to unreachable states.

   Description: 

     It cannot be proven (and it is not sound to assume) that applying
     method contracts in reachable Java states again leads to program
     states reachable in Java (it is not asserted that
     "inReachableState" holds in the post-state of a method). This is
     annoying, because loop invariants specified in JML implicitly
     contain "inReachableState".

   Workaround: 

     Manually remove the "inReachableState" from loop invariants.

   Plan: 

     Will be resolved in the future with the new method contract
     implementation.

7) \old is not supported in loop invariants.

8) Correctness proof obligations for taclets are unsound.

   Description: 

     Not all taclet features are supported by the generator of proof
     obligations that ensure soundness of user-defined lemma
     taclets. Taclets with such unsupported feature are not in all
     cases rejected, however. This makes it possible to load unsound
     taclets as lemmas during a proof.

   Plan: 

     The check will be made restrictive so that only proof-obligations 
     for taclets are generated that can be actually treated.