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

Re: [PVS-Help] PVS does not generate a disjointness TCC for embedded COND



Hi Jonathan,

Could you try out the following patch file, and let me know if it improves
things?

Thanks,
Sam

;; Fix for bug reported by Jonathan Ostroff on 2015-10-16
;; Incorrect cond TCCs

(in-package :pvs)

(defun generate-cond-disjoint-tcc (expr conditions values)
  (let* ((*old-tcc-name* nil)
	 (ndecl (make-cond-disjoint-tcc expr conditions values)))
    (if ndecl
	(insert-tcc-decl 'disjointness expr nil ndecl)
	(add-tcc-comment 'disjointness expr nil))))

(defun generate-cond-coverage-tcc (expr conditions)
  (let* ((*old-tcc-name* nil)
	 (ndecl (make-cond-coverage-tcc expr conditions)))
    (if ndecl
	(insert-tcc-decl 'coverage expr nil ndecl)
	(add-tcc-comment 'coverage expr nil))))

(defmethod set-type* ((expr first-cond-expr) expected)
  (declare (ignore expected))
  (let ((*ignore-else-part-tccs* nil))
    (call-next-method)
    (generate-cond-tccs expr)))

(defmethod set-type* ((expr single-cond-expr) expected)
  (declare (ignore expected))
  (let ((*ignore-else-part-tccs* nil))
    (call-next-method)
    (generate-cond-tccs expr)))

Jonathan Ostroff <jonathan@xxxxxxxx> wrote:

> HI Sam:
> 
> It looks like a disjointness TCC is overlooked when COND is embedded. The theory below type checks, but should not.
> 
> Is this a bug?
> 
> Regards
> 
> Jonathan
> 
> -----------------------------------------------------------------------------
> embedded_cond_bug: THEORY
> BEGIN
>   x,y,z: real
>   b: nat
>   
>   f:bool =
>     COND
>       x < 0 -> b = 0,     
>       x >= 0 ->
>         COND
> 	  x = 0 -> b =1,
> 	  x > 0 ->
> 	    COND
> 	      y <= 0 -> b = 2,
> 	      y >= 0 -> b = 3
> 	    ENDCOND
> 	ENDCOND
>     ENDCOND
> 
> END embedded_cond_bug
> 
> % Type-checking the above theory M-x tcp results in all 4 TCCS proved.
> 
> % This is incorrect as the third embedded COND is complete but not disjoint.
> 
> % The TCC below should not reduce to TRUE
> 
> % % The disjointness TCC (at line 7, column 4) in decl f for
> %     %  COND x < 0 -> b = 0,
> %     %      x >= 0 ->
> %     %        COND x = 0 -> b = 1,
> %     %             x > 0 -> COND y <= 0 -> b = 2, y >= 0 -> b = 3 ENDCOND
> %     %        ENDCOND
> %     % ENDCOND
> %   % was not generated because it simplifies to TRUE.
>