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

Re: [PVS-Help] Best practices for scientific notation in PVS?

Hi Cesar,

Thanks for the tip. I imagine that if I’m using these inside a large lookup table, then I could create a strategy that named the values and then used the eval-expr strategy, correct?

Best Regards,
Ben Hocking

On Aug 25, 2015, at 2:54 PM, MUNOZ, CESAR (LARC-D320) <cesar.a.munoz@xxxxxxxx> wrote:

You can use (eval-expr "c") and (eval-expr "e") to ground evaluate those constants when the actual values are needed. 


On Aug 25, 2015, at 12:53 PM, Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:

Another issue with using the x * 10^y format that I’ve encountered is that when y is largish, there’s the issue that when doing proofs, you have to rewrite 10^y as expt(10, y), which then gets rewritten as y * expt(10, y-1), etc., until you get to y-y and end up with 1. I suppose the other answer is to have tools that are generating this to just generate 299792458 in the one case (not so bad) and 0.000000000000000000160217662 in the other (a little long looking, and even worse for larger y, of course).

Best Regards,
Ben Hocking

On Aug 24, 2015, at 4:37 PM, Ben Hocking <ben.hocking@xxxxxxxxxxxxxxxxxxxxxxx> wrote:

So, I know that I can use:
  c: real = 2.99792458 * 10^8
  e: real = 1.60217662 * 10^-19
to represent scientific notation. However, is there a more “traditional” way to do this within PVS?

I’ve tried “1.60217662E-19” (both upper- and lower-case ‘e’) and likewise with “D/d” and “G/g”. I even tried it with the special unicode character (U+23E8, ⏨) and with the “\” character à la Algol.

This leads me to suspect that “ * 10^” is the string I should be using in lieu of “E” (etc.) when representing scientific notation in PVS, but I just wanted to see if this is indeed the recommended best practice.

Best Regards,
Ben Hocking