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?
You can use (eval-expr "c") and (eval-expr "e") to ground evaluate those constants when the actual values are needed.
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).
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.