[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] Problem with completeness check of COND



COND  FALSE -> FALSE ENDCOND should, presumably, be caught by the type checker as being incomplete. In  C_MD_ft_correct, below, that is what happens.

However, in  C_MD_ft_bad, all the type correctness proofs pass. This is presumably a bug?

Thanks,

Jonathan



===

foo_bar : THEORY

  BEGIN
    
    range_switch:  TYPE = {on, off}
    range_mode:    TYPE = {md_off, init, normal, failed}

    M_SW: VAR[nat -> range_switch]
    C_MD: VAR[nat -> range_mode]

    C_MD_ft_bad(M_SW, C_MD)(i:nat): bool =
     COND
	i = 0 -> C_MD(0) = md_off,
	i > 0 ->
	COND
		M_SW(i) = on -> C_MD(i) = md_off,
		M_SW(i) = off ->
		COND  FALSE -> FALSE ENDCOND
	ENDCOND	
   ENDCOND 

    C_MD_ft_correct(M_SW, C_MD)(i:nat): bool =
     COND
	i = 0 -> C_MD(0) = md_off,
	i > 0 ->
	COND
		M_SW(i) = off ->
		COND  FALSE -> FALSE ENDCOND,
		M_SW(i) = on -> C_MD(i) = md_off
	ENDCOND	
   ENDCOND 

 % Proof summary for theory foo_bar
 %    C_MD_ft_bad_TCC1......................proved - complete   [shostak](0.01 s)
 %    C_MD_ft_bad_TCC2......................proved - complete   [shostak](0.01 s)
 %    C_MD_ft_bad_TCC3......................proved - complete   [shostak](0.01 s)
 %    C_MD_ft_bad_TCC4......................proved - complete   [shostak](0.00 s)
 %    C_MD_ft_correct_TCC1..................unfinished          [shostak](0.02 s)
 %    Theory totals: 5 formulas, 5 attempted, 4 succeeded (0.06 s)

  END foo_bar