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

[Saswata Paul <paulsaswata1@xxxxxxxxx>]

Hi,

   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.