Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools

PVS Bug 456


Synopsis:        loop in type checker (PVS 2.3 with or without patches)
Severity:        serious
Priority:        medium
Responsible:     owre
State:           analyzed
Class:           sw-bug
Arrival-Date:    Thu Apr  6 01:40:00 2000
Originator:      Paul Y Gloess
Organization:    labri.u-bordeaux.fr
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  This is a multi-part message in MIME format.
  --------------DED084B31C92EFF08843A027
  Content-Type: text/plain; charset=us-ascii
  Content-Transfer-Encoding: 7bit
  
  Hi:
  
  I found a situation where PVS 2.3 (or PVS 2.3 (patch level 1.2.2.36))
  type checker enters a loop.
  
  This bug is related to specific judgements: they are commented out in
  the attached  dump, so that it could be produced. To reproduce the bug,
  one has to remove the comments, as explained in dumped theories. Note
  that the dump also illustrates a crash problem (already encountered and
  reported) with Meta-X show-tccs.
  
  I have two questions:
  
  a) would it be considered OK for the PVS prover not to terminate because
  of judgements (as it may happen with a bad set of auto-rewrite rules)?
             I would tend to think that judgements are handled in a
  different way, and should be safe;
  b) should PVS type checker always terminate?
             I would definitely say yes.
  
  Anyway, I would be comforted to have your own opinion.
  
  
  Best regards!
  
       paul
  
  --------------DED084B31C92EFF08843A027
  Content-Type: text/plain; charset=us-ascii;
   name="bug.tcc_loop.29_march_2000.isequences.dump"
  Content-Transfer-Encoding: 7bit
  Content-Disposition: inline;
   filename="bug.tcc_loop.29_march_2000.isequences.dump"
  
  
  $$$isequences.pvs
  %%%
  %%% Paul Y Gloess <Paul.Gloess@LaBRI.U-Bordeaux.Fr>
  %%%   http://dept-info.labri.u-bordeaux.fr/~gloess/
  %%%   http://www.enserb.fr/~gloess/
  %%%
  %%% Bug report, 29 march 2000, with PVS 2.3 (no patch):
  %%%
  %%% This theory does not type check in finite time
  %%%  when "co_succ_co" judgement is activated in
  %%%  imported theory "intervals" (by removing
  %%%  comment). See "intervals" theory for details.
  %%%
  isequences[T: TYPE]: THEORY
  
    BEGIN
  
      IMPORTING intervals
  
      %%
      %% Composition of an infinite sequence u of finite sequences:
      %%   u0: [cc(c0, c1)->T], ..., un: [cc(cn, cn+1)->T], ...
      %%   assuming that c is a nat cover (see "intervals" theory):
      %%
      compose(c: (nat_cover?))
             (u: [n: nat -> [cc(c(n), c(n+1)) -> T]])
             (k: nat)
        : T
        = u(choose({n: nat | co?(c(n), c(n+1))(k)}))(k) ; % choose from singlet
 on.
  
      nat_cover_seq?(c: (nat_cover?))
                    (u: [n: nat -> [cc(c(n), c(n+1)) -> T]])
        : bool
        = (FORALL (n: nat): u(n)(c(n+1)) = u(n+1)(c(n))) ;
  
      relation_compose: LEMMA
        (FORALL (R: [T, T -> bool], c: (nat_cover?),
                 u: (nat_cover_seq?(c))):
          (FORALL (n: nat):
             R(compose(c)(u)(n), compose(c)(u)(1+n)))
             =
          (FORALL (n: nat, k: co(c(n), c(1+n))):
             R(u(n)(k), u(n)(1+k)))) ;
  
    END isequences
  
  $$$isequences.prf
  (|isequences|
   (|compose_TCC1| "" (SUBTYPE-TCC) NIL NIL)
   (|compose_TCC2| "" (SUBTYPE-TCC) NIL NIL)
   (|compose_TCC3| "" (SKOLEM * ("c" "k" "u"))
    (("" (EXPAND "cc?") (("" (EXPAND "co?") (("" (GROUND) NIL NIL)) NIL))
      NIL))
    NIL)
   (|compose_TCC4| "" (SKOLEM * ("c" "k" "u"))
    (("" (EXPAND "nonempty?")
      (("" (EXPAND "empty?")
        (("" (EXPAND "member")
          (("" (EXPAND "co?")
            (("" (REWRITE "forall_not")
              (("" (REWRITE "nat_cover_covers") NIL NIL)) NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL)
   (|relation_compose| "" (SKOLEM * ("R" "c" "u"))
    (("" (AUTO-REWRITE "nat_cover_nat")
      (("" (IFF)
        (("" (PROP)
          (("1" (SKOLEM * ("n" "k"))
            (("1" (TYPEPRED "k")
              (("1" (INST * "k")
                (("1" (EXPAND "compose") (("1" (POSTPONE) NIL NIL)) NIL)
                 ("2" (EXPAND "co?") (("2" (GROUND) NIL NIL)) NIL))
                NIL))
              NIL))
            NIL)
           ("2" (POSTPONE) NIL NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  
  
  $$$intervals.pvs
  %%%
  %%% Paul Y Gloess <Paul.Gloess@LaBRI.U-Bordeaux.Fr>
  %%%   http://dept-info.labri.u-bordeaux.fr/~gloess/
  %%%   http://www.enserb.fr/~gloess/
  %%%
  %%% This theory type checks, but there are two problems
  %%%  arising upon uncommenting "co_succ_co" judgement:
  %%%  a) <Meta-X>show-tccs crashes;
  %%%  b) type-checker loop for importing theory "isequences".
  %%%
  intervals: THEORY
  
    BEGIN
  
      %%
      %% Intervals [a, b[:
      %%
      co?(a, b: int)(n: int)
        : bool
        = a <= n  AND  n < b ;
  
      co(a, b: int): TYPE = (co?(a, b)) ;
  
      %%
      %% Intervals [a, b]:
      %%
      cc?(a, b: int)(n: int)
        : bool
        = a <= n  AND  n <= b ;
  
      cc(a, b: int): TYPE = (cc?(a, b)) ;
  
  %%%
  %%% This JUDGEMENT types check ok, but yields TC loop in importing theory
  %%%  "isequences": remove comments to reproduce bug.
  %%%
  %   co_succ_co: JUDGEMENT
  %     co(a, b: int) SUBTYPE_OF co(a, 1+b) ;
  
  
      %%
      %% A nat cover is a sequence c0=0<c1<c2< ... <cn<cn+1<...
      %%
      nat_cover?(c: [nat -> nat]): bool
        = (c(0)=0  AND  (FORALL (k: nat): c(k)<c(k+1))) ;
  
    END intervals
  
  $$$intervals.prf
  (|intervals|
   (|co_succ_co| "" (SUBTYPE-TCC) NIL NIL))
  
  
  --------------DED084B31C92EFF08843A027--

How-To-Repeat: 

Fix: 
1. Modified typecheck* (subtype-judgement) to reset the print-type to
   remove the types form the type-application; otherwise the TCC won't
   print correctly.
2. Modified subtype-of? to let *subtypes-matched* to nil - used in
   find-known-subtypes to control looping.
3. Modified find-known-subtypes* to check for and push used knonw-subtypes
   into *merged-subtypes* so as to break loops.
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools