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

[Apostolis Xekoukoulotakis <apostolis.xekoukoulotakis@xxxxxxxxx>]

In TLA, we can have two algorithms A and B where A refines B. So you need to specify an abstract algorithm and a more concrete one and then check with TLC (or prove) that it is a refinement.

On Tue, Feb 12, 2019 at 7:50 PM Saswata Paul <paulsaswata1@xxxxxxxxx> wrote:

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.

-- 
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.