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

[tlaplus] Can TLA+ be used to verify algorithms with a level of abstraction?


   I have an algorithm that I want to prove is correct. I have already proven that it is correct in a human-readable proof by using induction. However, the actual implementation of the code in python is very large. I was wondering if TLA+ a suitable language for writing algorithms with a level of abstraction and formally verifying that the loop invariants and procedure pre/postconditions hold.
   PS. - I am new to formal verification and TLA+ seems like the tool with the best online support and a good IDE.  
Thank you   

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+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.