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

Re: K_conversion

I too have been repeatedly bitten by PVS overzealously applying
conversions.  I have most recently been bothered by PVS
inappropriately applying the `extend' conversion.  I heartily endorse
having the option to turn automatic conversions off.  In fact, I would 
prefer that that be the default case.  

I would also like the option of preventing PVS from simplifying
arithmetic expressions.  For example, expressions like:
   (t - s)*(1 + rho)
are often easier to work with than
   t + t*rho - s - s*rho
when doing proofs clock synchronization.

In cases like these, interacting with PVS is somewhat like using
Microsoft Word.  Much time is wasted trying to undo and work around
the effects of built-in automation.


-- Paul S. Miner                | phone: (757) 864-6201
-- 1 South Wright St. / MS 130  | fax:   (757) 864-4234
-- NASA Langley Research Center | mailto:p.s.miner@larc.nasa.gov
-- Hampton, Virginia 23681-2199 | http://shemesh.larc.nasa.gov/~psm/