Email Gateway (Aug 23 2022 at 09:17): Email Gateway (Aug 23 2022 at 09:17):From: Yakoub Nemouchi <y.nemouchi@gmail.com>
For advanced knowledge, you can read:
http://www-wjp.cs.uni-saarland.de/leute/private_homepages/nschirmer/pub/schirmer_phd.pdf
Very well written and explained PhD thesis.
There is also something for whitebox testing
:
https://www.isa-afp.org/entries/Clean.html
For very basic and very well explained knowledge on the topic, I would also
ask Peter Lammich or Tobias Nipkow for IMP slides or lecture material, if
it is possible to be shared (I am being naive here since I do not know the
Universities policies about sharing lecture slide it might be complicated).
It might be the case that http://www.concrete-semantics.org, is more than
enough for very basic knowledge on the topic.
Best wishes,
Yakoub.
Email Gateway (Aug 23 2022 at 09:24):From: Alex Meyer <alex153@outlook.lv>
Hello!
I posted conceptual question in stackoverflow https://stackoverflow.com/questions/62709073/how-to-model-formalize-the-change-of-the-variable-change-of-world-in-isabelle but I am re-posting here as well. Maybe someone can give us some clarification. Thanks!
I am trying to formalize business rules in Isabelle/HOL, but business rules involve the change of the values of some variables, like if x=5 => x=6. => is not the usual implication there, because x is 5 in one world (interpretation, semantic domain) and after the execution of the rule the x is 6 and it is already a different world (different interpretation, assignment function, semantic domain). So - technically is x=5 => x=6 is not the formula in First Order Logic and it is not also the formula of Higher Order Logic of Isabelle/HOL. More possible is that it is the formula in dynamic/action logic [rule1](x=5)=(x=6) (that defines that upon application of rule1 to the formula in some world yields to the truthful formula in some other world (dynamic/action logic is essentially a kind of modal logic and Kripke/possible world semantics can be applied here).
Now, back to Isabelle/HOL or Coq: FOL/HOL theory is set of formulas in all the worlds or in one particular world. If we stay at FOL/HOL then there is no change of the world, no change of the values of the variables. We should go to the modal logics if we would like to model, reasong about such changes. But can it be done in HOL? This change of world?
http://matryoshka.gforge.inria.fr/pubs/fernandez_burgos_bsc_thesis.pdf is good work about formalization of sorting algorithms in Isabelle/HOL, functional programming is used there and there is no need of variables and hence - no this change among worlds. But if we try to model Reinforcement Learning, Markov processes, impertative/object oriented programming, business rules in Isabelle/HOL, then we should express this change. How to do that?
How to express business rule if x=5 => x=6 in Isabelle/HOL?
Alex
[https://ipmcdn.avast.com/images/icons/icon-envelope-tick-green-avg-v1.png]<http://www.avg.com/email-signature?utm_medium=email&utm_source=link&utm_campaign=sig-email&utm_content=webmail> Virus-free. www.avg.com<http://www.avg.com/email-signature?utm_medium=email&utm_source=link&utm_campaign=sig-email&utm_content=webmail>
Email Gateway (Aug 23 2022 at 09:25):From: "lammich@in.tum.de" <lammich@in.tum.de>
Hi Alex
A standard approach might be a deep embedding, eg as a state transition system
on top of hol.
Peter
Email Gateway (Aug 23 2022 at 09:26):From: Mark Wassell <mpwassell@gmail.com>
Following on from Peter's response, and if you want to take a programming
language view of what you are doing, there are a number of formalisations
of imperative languages in the AFP, for example
https://www.isa-afp.org/entries/IMP2.html, and there is also a book that
covers the semantics of an imperative language,
http://www.concrete-semantics.org.
Mark
Last updated: Apr 24 2024 at 20:16 UTC