Thank you, Stephan, for the suggestions and the kind welcome.
About getting benefit from the TLA+ / PlusCal environment, yes, I would like to be able to describe algorithms in a reasonably abstract way and in multiple forms that might include various approaches for parallelism. Prior to this, I spent some time with SPIN and considered implementing checks in C (somewhat like Pamela Zave did with the Chord protocol). Not sure if TLA+ might accommodate that kind of thing.
More generally, though, how does one say what it means for (certain types of) numerical programs to be correct? A simple declarative statement (like Ax = b) at the termination of an iterative algorithm would be easy to state but impossible to prove (within the framework, e.g., convergence of a fixed point computation).
The real value would come, I feel, in something akin to refinement checking in FDR3, which would be ideal for the problems I'm looking at (but with PlusCal instead of CSP). I think that's hard to come by. That's what led me to think about building up symbolic expressions and comparing them in various ways, while relying on TLA+ / PlusCal as the overall framework.
As an aside, I'm coming to TLA+ from the applications side (civil engineering) instead of theory, though I do have some experience with other tools like the Concurrency Workbench, LTSA/FSP, and, long before that, the Larch family of provers.
Thanks,
John
On Friday, September 12, 2014 12:47:37 PM UTC-4, Stephan Merz wrote:
Hello John,
welcome to the TLA+ group.
Your project sounds interesting. However, first it is not clear to me that what you are proposing is restricted to PlusCal in any way. Remember that PlusCal is getting translated to TLA+ and that the ordinary TLA+ tools (TLC and the prover) are used on the result of the translation.
Second, what would your back-end for comparing these expressions actually be? The existing tools will not natively support the symbolic computations that you are interested in, although you can use them for testing assertions on fixed values, as you say.
If you are focusing on symbolic comparisons of polynomials, using a dedicated solver such as Redlog (http://www.redlog.eu) may be the easier path – assuming you do not get any benefit from the TLA+ / PlusCal environment.
Best,
Stephan
On 12 Sep 2014, at 18:34, jwb...@xxxxxxxxx wrote:
> Hi everyone,
>
> I would like to compare, symbolically, some mathematical expressions that get built up in a numerical application I am specifying in PlusCal. My first thought is to write a module for multivariate polynomials and use it in place of PlusCal's built-in arithmetic operations. I would then make intermittent assertions about polynomials and check them for functional correctness with TLC.
>
> For my application, I believe this "symbolic" approach is a better fit than a discrete sampling from real numbers.
>
> If anyone has thoughts or suggestions, however, I would be much obliged.
>
> Thanks,
> John
>
> --
> You received this message because you are subscribed to the Google Groups "tlaplus" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
> To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
> Visit this group at http://groups.google.com/group/tlaplus.
> For more options, visit https://groups.google.com/d/optout.