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

PVS Bug 465


Synopsis:        Bugs in recognizer types vs. ADT's
Severity:        serious
Priority:        medium
Responsible:     dave_sc (Dave Stringer-Calvert)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Tue Jun 20 11:00:01 2000
Originator:      "Ralph D. Jeffords"
Organization:    itd.nrl.navy.mil
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  ----------
  X-Sun-Data-Type: text
  X-Sun-Data-Description: text
  X-Sun-Data-Name: text
  X-Sun-Charset: us-ascii
  X-Sun-Content-Lines: 6
  
  Here are a couple of related bugs that both seem to be some inconsistent
  interaction between "recognizer union types" and whether you use external
  ADT's or put them inline. In the case of recognizer_type_bug the error
  presents itself as failure to type check, while in recognizer_type_bug2 the
  error presents as something incorrectly generated by show-tccs/ppe that
  won't parse. Detailed explanation is in the files.
  ----------
  X-Sun-Data-Type: default
  X-Sun-Data-Description: default
  X-Sun-Data-Name: recognizer_type_bug.dmp
  X-Sun-Charset: us-ascii
  X-Sun-Content-Lines: 58
  
  %Patch files loaded: patch2 version 1.2.2.36
  
  $$$recognizer_type_bug.pvs
  %========================================================
  % Bug in recognizer union types vs. external ADT's
  %
  % There is a type checking error for the following theory:
  %
  %       Could not determine the full theory instance for F
  %         Theory instance: recognizer_type_bug
  %
  % However, if you comment out the IMPORTING clause and
  % uncomment and use the inline version of list then
  % everything is ok.
  %
  % 20 june 2000
  %========================================================
  recognizer_type_bug [ T: TYPE]: THEORY
  BEGIN
  
  	IMPORTING list[T]
  
  
  %list : DATATYPE 
  % BEGIN
  %  null: null?
  %  cons (car: T, cdr:list):cons?
  % END list
  
  
  	t: VAR T
  	L,L_: VAR list
  
  recognizers(L):TYPE =
  
  	{ L_ |	CASES L OF
  		  null: 	null?(L_),
  		  cons(t,L__):  cons?(L_)
  		ENDCASES }
  
  
  
  F(L,t):  RECURSIVE recognizers(L) =
  
  	CASES L OF
  	  null:		null,
  	  cons(t_,L_):	cons(t_,F(L_,t))
  	ENDCASES
  	MEASURE reduce_nat(1,LAMBDA t,(i:nat): i+1)(L)
  
  
  END recognizer_type_bug
  
  $$$recognizer_type_bug.prf
  (|recognizer_type_bug| (F_TCC1 "" (SUBTYPE-TCC) NIL NIL)
   (F_TCC2 "" (TERMINATION-TCC) NIL NIL)
   (F_TCC3 "" (SUBTYPE-TCC) NIL NIL))
  
  ----------
  X-Sun-Data-Type: default
  X-Sun-Data-Description: default
  X-Sun-Data-Name: recognizer_type_bug2.dmp
  X-Sun-Charset: us-ascii
  X-Sun-Content-Lines: 381
  
  %Patch files loaded: patch2 version 1.2.2.36
  
  $$$recognizer_type_bug2.pvs
  %========================================================
  % Bug in recognizer union types
  %
  % NOTE: this is filtered from an example of representing
  % the Lambda Calculus in PVS developed by Sylvan Pinsky
  %
  % 20 june 2000
  %========================================================
  recognizer_type_bug2 [ ID: TYPE+]: THEORY
  BEGIN
  
  	IMPORTING term[ID]
  
  %term: DATATYPE
  %BEGIN
  %	vble(x:ID):vble?
  %	app(U,V:term):app?
  %	abs(y:ID,E:term):abs?
  %END term
  
  	y: VAR ID
  	W,E_: VAR term
  
  recognizers(W):TYPE =
  
  	{ E_ |	CASES W OF
  		  vble(x):	vble?(E_),
  		  app(U,V):	app?(E_),
  		  abs(x,E):	abs?(E_)
  		ENDCASES }
  
  
  recognizers?(W)(E_):boolean =
  
  			CASES W OF
  			   vble(x): vble?(E_),
  			   app(U,V): app?(E_),
  			   abs(x,E): abs?(E_)
  			 ENDCASES
  
  %------------------------------------------------------------
  % Various combinations of 
  %
  % (1) whether you use the ADT "term" inline vs. external version
  %
  % (2) which of three different signatures you use for F
  %
  % give different behavior when they should ALL be okay:
  %
  % 		inline "term"		external "term"
  %	-----------------------------------------------
  %	|
  % (1) F |	okay			okay
  %	|
  % (2) F |	okay			ppe/show_tccs error
  %	|
  % (3) F |	okay			ppe/show_tccs error
  %	|
  %
  % The ppe/show_tccs error is that when you invoke either
  % command you get
  %
  %  Found [ when expecting
  %    : or (
  %
  % and PVS arbitrarily replaces the main buffer with
  % some other buffer.
  %
  % In all the cases the TCC's will prove---you just cannot
  % view them via show_tccs/ppe in the two error cases.
  %------------------------------------------------------------
  
  % (1)
  %F(W,y): RECURSIVE  (recognizers?(W))  =
  
  % (2)
  F(W,y): RECURSIVE  recognizers(W)  =	
  
  % (3)
  %F(W,y): RECURSIVE { E_ | CASES W OF vble(x):vble?(E_),
  %		  	    app(U,V):	app?(E_),
  %		  	    abs(x,E):	abs?(E_)
  %			  ENDCASES } =
  
  
  	CASES W OF
  	  vble(x):	vble(y),
  	  app(U,V):	app(F(U,y),F(V,y)),
  	  abs(x,E):	abs(x,F(E,y))
  	ENDCASES
  	MEASURE W by <<	 
  
  
  END recognizer_type_bug2
  
  $$$recognizer_type_bug2.prf
  (|recognizer_type_bug2|
   (F_TCC1 "" (USE "term_well_founded") (("" (GRIND) NIL NIL)) NIL)
   (F_TCC2 "" (SUBTYPE-TCC) NIL NIL)
   (F_TCC3 "" (TERMINATION-TCC) NIL NIL)
   (F_TCC4 "" (TERMINATION-TCC) NIL NIL)
   (F_TCC5 "" (SUBTYPE-TCC) NIL NIL)
   (F_TCC6 "" (TERMINATION-TCC) NIL NIL)
   (F_TCC7 "" (SUBTYPE-TCC) NIL NIL))
  
  
  $$$term_adt.pvs
  %%% ADT file generated from term
  
  term_adt[T: TYPE+]: THEORY
   BEGIN
    ASSUMING
     T_TCC1: ASSUMPTION EXISTS (x: T): TRUE;
    ENDASSUMING
  
    term: TYPE
  
    vble?, app?, abs?: [term -> boolean]
  
    vble: [T -> (vble?)]
  
    x: [(vble?) -> T]
  
    app: [[term, term] -> (app?)]
  
    U: [(app?) -> term]
  
    V: [(app?) -> term]
  
    abs: [[T, term] -> (abs?)]
  
    y: [(abs?) -> T]
  
    E: [(abs?) -> term]
  
    ord(x1: term): upto(2) =
        CASES x1
          OF vble(vble1_var): 0,
             app(app1_var, app2_var): 1,
             abs(abs1_var, abs2_var): 2
          ENDCASES
  
    term_vble_extensionality: AXIOM
      FORALL (vble?_var: (vble?), vble?_var2: (vble?)):
        x(vble?_var) = x(vble?_var2) IMPLIES vble?_var = vble?_var2;
  
    term_vble_eta: AXIOM
      FORALL (vble?_var: (vble?)): vble(x(vble?_var)) = vble?_var;
  
    term_app_extensionality: AXIOM
      FORALL (app?_var: (app?), app?_var2: (app?)):
        U(app?_var) = U(app?_var2) AND V(app?_var) = V(app?_var2) IMPLIES
         app?_var = app?_var2;
  
    term_app_eta: AXIOM
      FORALL (app?_var: (app?)): app(U(app?_var), V(app?_var)) = app?_var;
  
    term_abs_extensionality: AXIOM
      FORALL (abs?_var: (abs?), abs?_var2: (abs?)):
        y(abs?_var) = y(abs?_var2) AND E(abs?_var) = E(abs?_var2) IMPLIES
         abs?_var = abs?_var2;
  
    term_abs_eta: AXIOM
      FORALL (abs?_var: (abs?)): abs(y(abs?_var), E(abs?_var)) = abs?_var;
  
    term_x_vble: AXIOM FORALL (vble1_var: T): x(vble(vble1_var)) = vble1_var;
  
    term_U_app: AXIOM
      FORALL (app1_var: term, app2_var: term):
        U(app(app1_var, app2_var)) = app1_var;
  
    term_V_app: AXIOM
      FORALL (app1_var: term, app2_var: term):
        V(app(app1_var, app2_var)) = app2_var;
  
    term_y_abs: AXIOM
      FORALL (abs1_var: T, abs2_var: term):
        y(abs(abs1_var, abs2_var)) = abs1_var;
  
    term_E_abs: AXIOM
      FORALL (abs1_var: T, abs2_var: term):
        E(abs(abs1_var, abs2_var)) = abs2_var;
  
    term_inclusive: AXIOM
      FORALL (term_var: term):
        vble?(term_var) OR app?(term_var) OR abs?(term_var);
  
    term_induction: AXIOM
      FORALL (p: [term -> boolean]):
        ((FORALL (vble1_var: T): p(vble(vble1_var))) AND
          (FORALL (app1_var: term, app2_var: term):
             p(app1_var) AND p(app2_var) IMPLIES p(app(app1_var, app2_var)))
           AND
           (FORALL (abs1_var: T, abs2_var: term):
              p(abs2_var) IMPLIES p(abs(abs1_var, abs2_var))))
         IMPLIES (FORALL (term_var: term): p(term_var));
  
    every(p: PRED[T])(a: term):  boolean =
        CASES a
          OF vble(vble1_var): p(vble1_var),
             app(app1_var, app2_var):
               every(p)(app1_var) AND every(p)(app2_var),
             abs(abs1_var, abs2_var): p(abs1_var) AND every(p)(abs2_var)
          ENDCASES;
  
    every(p: PRED[T], a: term):  boolean =
        CASES a
          OF vble(vble1_var): p(vble1_var),
             app(app1_var, app2_var):
               every(p, app1_var) AND every(p, app2_var),
             abs(abs1_var, abs2_var): p(abs1_var) AND every(p, abs2_var)
          ENDCASES;
  
    some(p: PRED[T])(a: term):  boolean =
        CASES a
          OF vble(vble1_var): p(vble1_var),
             app(app1_var, app2_var): some(p)(app1_var) OR some(p)(app2_var),
             abs(abs1_var, abs2_var): p(abs1_var) OR some(p)(abs2_var)
          ENDCASES;
  
    some(p: PRED[T], a: term):  boolean =
        CASES a
          OF vble(vble1_var): p(vble1_var),
             app(app1_var, app2_var): some(p, app1_var) OR some(p, app2_var),
             abs(abs1_var, abs2_var): p(abs1_var) OR some(p, abs2_var)
          ENDCASES;
  
    subterm(x1, y1: term):  boolean =
        x1 = y1 OR
         CASES y1
           OF vble(vble1_var): FALSE,
              app(app1_var, app2_var):
                subterm(x1, app1_var) OR subterm(x1, app2_var),
              abs(abs1_var, abs2_var): subterm(x1, abs2_var)
           ENDCASES;
  
    <<(x1, y1: term):  boolean =
        CASES y1
          OF vble(vble1_var): FALSE,
             app(app1_var, app2_var):
               (x1 = app1_var OR x1 << app1_var) OR
                x1 = app2_var OR x1 << app2_var,
             abs(abs1_var, abs2_var): x1 = abs2_var OR x1 << abs2_var
          ENDCASES;
  
    term_well_founded: AXIOM well_founded?[term](<<);
  
    reduce_nat(vble?_fun: [T -> nat], app?_fun: [[nat, nat] -> nat],
               abs?_fun: [[T, nat] -> nat]):
     [term -> nat] =
        LAMBDA (term_adtvar: term):
          LET red: [term -> nat] = reduce_nat(vble?_fun, app?_fun, abs?_fun)
            IN
            CASES term_adtvar
              OF vble(vble1_var): vble?_fun(vble1_var),
                 app(app1_var, app2_var):
                   app?_fun(red(app1_var), red(app2_var)),
                 abs(abs1_var, abs2_var): abs?_fun(abs1_var, red(abs2_var))
              ENDCASES;
  
    REDUCE_nat(vble?_fun: [[T, term] -> nat],
               app?_fun: [[nat, nat, term] -> nat],
               abs?_fun: [[T, nat, term] -> nat]):
     [term -> nat] =
        LAMBDA (term_adtvar: term):
          LET red: [term -> nat] = REDUCE_nat(vble?_fun, app?_fun, abs?_fun)
            IN
            CASES term_adtvar
              OF vble(vble1_var): vble?_fun(vble1_var, term_adtvar),
                 app(app1_var, app2_var):
                   app?_fun(red(app1_var), red(app2_var), term_adtvar),
                 abs(abs1_var, abs2_var):
                   abs?_fun(abs1_var, red(abs2_var), term_adtvar)
              ENDCASES;
  
    reduce_ordinal(vble?_fun: [T -> ordinal],
                   app?_fun: [[ordinal, ordinal] -> ordinal],
                   abs?_fun: [[T, ordinal] -> ordinal]):
     [term -> ordinal] =
        LAMBDA (term_adtvar: term):
          LET red: [term -> ordinal] =
                reduce_ordinal(vble?_fun, app?_fun, abs?_fun)
            IN
            CASES term_adtvar
              OF vble(vble1_var): vble?_fun(vble1_var),
                 app(app1_var, app2_var):
                   app?_fun(red(app1_var), red(app2_var)),
                 abs(abs1_var, abs2_var): abs?_fun(abs1_var, red(abs2_var))
              ENDCASES;
  
    REDUCE_ordinal(vble?_fun: [[T, term] -> ordinal],
                   app?_fun: [[ordinal, ordinal, term] -> ordinal],
                   abs?_fun: [[T, ordinal, term] -> ordinal]):
     [term -> ordinal] =
        LAMBDA (term_adtvar: term):
          LET red: [term -> ordinal] =
                REDUCE_ordinal(vble?_fun, app?_fun, abs?_fun)
            IN
            CASES term_adtvar
              OF vble(vble1_var): vble?_fun(vble1_var, term_adtvar),
                 app(app1_var, app2_var):
                   app?_fun(red(app1_var), red(app2_var), term_adtvar),
                 abs(abs1_var, abs2_var):
                   abs?_fun(abs1_var, red(abs2_var), term_adtvar)
              ENDCASES;
   END term_adt
  
  term_adt_map[T: TYPE+, T1: TYPE+]: THEORY
   BEGIN
    ASSUMING
     T_TCC1: ASSUMPTION EXISTS (x: T): TRUE;
  
     T1_TCC1: ASSUMPTION EXISTS (x: T1): TRUE;
    ENDASSUMING
  
    IMPORTING term_adt
  
    map(f: [T -> T1])(a: term[T]):  term[T1] =
        CASES a
          OF vble(vble1_var): vble(f(vble1_var)),
             app(app1_var, app2_var):
               app(map(f)(app1_var), map(f)(app2_var)),
             abs(abs1_var, abs2_var): abs(f(abs1_var), map(f)(abs2_var))
          ENDCASES;
  
    map(f: [T -> T1], a: term[T]):  term[T1] =
        CASES a
          OF vble(vble1_var): vble(f(vble1_var)),
             app(app1_var, app2_var):
               app(map(f, app1_var), map(f, app2_var)),
             abs(abs1_var, abs2_var): abs(f(abs1_var), map(f, abs2_var))
          ENDCASES;
   END term_adt_map
  
  term_adt_reduce[T: TYPE+, range: TYPE]: THEORY
   BEGIN
    ASSUMING
     T_TCC1: ASSUMPTION EXISTS (x: T): TRUE;
    ENDASSUMING
  
    IMPORTING term_adt[T]
  
    reduce(vble?_fun: [T -> range], app?_fun: [[range, range] -> range],
           abs?_fun: [[T, range] -> range]):
     [term -> range] =
        LAMBDA (term_adtvar: term):
          LET red: [term -> range] = reduce(vble?_fun, app?_fun, abs?_fun) IN
            CASES term_adtvar
              OF vble(vble1_var): vble?_fun(vble1_var),
                 app(app1_var, app2_var):
                   app?_fun(red(app1_var), red(app2_var)),
                 abs(abs1_var, abs2_var): abs?_fun(abs1_var, red(abs2_var))
              ENDCASES;
  
    REDUCE(vble?_fun: [[T, term] -> range],
           app?_fun: [[range, range, term] -> range],
           abs?_fun: [[T, range, term] -> range]):
     [term -> range] =
        LAMBDA (term_adtvar: term):
          LET red: [term -> range] = REDUCE(vble?_fun, app?_fun, abs?_fun) IN
            CASES term_adtvar
              OF vble(vble1_var): vble?_fun(vble1_var, term_adtvar),
                 app(app1_var, app2_var):
                   app?_fun(red(app1_var), red(app2_var), term_adtvar),
                 abs(abs1_var, abs2_var):
                   abs?_fun(abs1_var, red(abs2_var), term_adtvar)
              ENDCASES;
   END term_adt_reduce
  $$$term.pvs
  %==============================
  % Datatype for lambda expressions
  %================================
  term[T: TYPE+]: DATATYPE
  BEGIN
  	vble(x:T):vble?
  	app(U,V:term):app?
  	abs(y:T,E:term):abs?
  END term

How-To-Repeat: 

Fix: 

 [davesc]
 Fixed in 2.3.1

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