Timeline for Program transformation as alternative for Hoare logic or temporal logic
Current License: CC BY-SA 3.0
7 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 31, 2011 at 20:10 | comment | added | Lucas K. | Andreas, I am not familiar with Coq, but I know a little ZFC and HOL Light. As far I know, if one has to transform a computerprogram with a loop to a logical expression in one of those systems, then you end up in making a closure operator somewhere. So, when explaining how programs and systems like ZFC and HOL light are related, then I think you have to start that. From there, one can go to fixed point theorems. I am an outsider, because I do not work on an university. But graduates that start to work in my company, are not capable of defining a mathematical problem in a formal system. | |
| Jul 30, 2011 at 10:27 | comment | added | Andrej Bauer | Sort of like this: cstheory.stackexchange.com/questions/7029/… | |
| Jul 30, 2011 at 10:26 | comment | added | Andrej Bauer | I was just commenting on your sweeping statement that "the known techniques are Hoare logic and temporal logics". There are many others. If you are going to educate people about loops, you should show them fixed points and explain how loops are a form of fixed points equations. That in my opinion is much more illuminating, and it is just stanard math (order theory). | |
| Jul 29, 2011 at 21:47 | comment | added | Lucas K. | Andrej, I am reading the tutorial of Minlog. On page 12, they do add-global-assumption. These kind of things you want to avoid, because this way you can introduce inconsistencies in your system. The way I define the predicate in my question is 'safe', because it is a single definition. Taking the transitive reflexive closure is also 'safe'. So, I define the Fibonacci numbers in a safe way, while the tutorial in Minlog isn't. | |
| Jul 29, 2011 at 21:27 | comment | added | Lucas K. | Thanks for the answer. But the other answer was more the answer I was looking for. Basically, I am looking for methods that are simpler and better accessible for people that are not expert in logic. For those people I think it is interesting to understand the relation between loops and closures. Where the loop is more about programming, the closure is more mathematical. So, this is the bridge between those 2. Coq is for non-logicians too complex. I will take a look at Minlog. | |
| Jul 21, 2011 at 6:54 | history | edited | Andrej Bauer | CC BY-SA 3.0 |
link to Agda; added 56 characters in body
|
| Jul 21, 2011 at 6:42 | history | answered | Andrej Bauer | CC BY-SA 3.0 |