Email Gateway (Aug 18 2022 at 11:11): Email Gateway (Aug 18 2022 at 11:11):From: Temesghen Kahsai <lememta@gmail.com>
On Jan 6, 2008 1:44 AM, Alessandro Cavalcante Gurgel <
rolangomaster@gmail.com> wrote:
Hi,
I'm Alessandro Gurgel, student of UFRN, Brazil. Currently, I am a
member of the project Circus Refine. The project is the development of a
tool that support the language Circus.Circus specifications combine both
data and behavioural aspects of concurrent systems using a combination of
CSP, Z, and Dijkstra's command language. Its associated refinement theory
and calculus distinguishes itself from other such combinations.So, we intend to integrate our CRefine tool with a theorem proving.
Isabelle seems to be a good theorem proving but we need some more
informations about this proof assistant.
Depending what you want to prove, you can have a look at Csp-Prover, which
is build upon Isabelle/HOL (
http://staff.aist.go.jp/y-isobe/CSP-Prover/CSP-Prover.html).
1- Isabelle is avaible in Windows ? it needs some kind of simulator as
cygwin ?
2- How coul we integrate our tool with Isabelle ? Do you have any
documentation about support for communication with external tools ?Thanks,
Alessandro
Email Gateway (Aug 18 2022 at 11:18):From: Alessandro Cavalcante Gurgel <rolangomaster@gmail.com>
Hi,
I'm Alessandro Gurgel, student of UFRN, Brazil. Currently, I am a
member of the project Circus Refine. The project is the development of a
tool that support the language Circus.Circus specifications combine both
data and behavioural aspects of concurrent systems using a combination of
CSP, Z, and Dijkstra's command language. Its associated refinement theory
and calculus distinguishes itself from other such combinations.
So, we intend to integrate our CRefine tool with a theorem proving.
Isabelle seems to be a good theorem proving but we need some more
informations about this proof assistant.
1- Isabelle is avaible in Windows ? it needs some kind of simulator as
cygwin ?
2- How coul we integrate our tool with Isabelle ? Do you have any
documentation about support for communication with external tools ?
Thanks,
Alessandro
Email Gateway (Aug 18 2022 at 11:19):From: Makarius <makarius@sketis.net>
On Sat, 5 Jan 2008, Alessandro Cavalcante Gurgel wrote:
Isabelle seems to be a good theorem proving but we need some more
informations about this proof assistant.1- Isabelle is avaible in Windows ? it needs some kind of simulator as
cygwin ?
Yes, thanks to the native Cygwin version of Poly/ML 5.0 and 5.1, Isabelle
now runs routinely under windows as well. Traditionally, the majority of
our users are on Linux or Mac OS X, but some people have now started to
use Windows/Cygwin more seriously.
Note that Cygwin is not a simulator, but a plain windows DLL that
essentially unleashes the well-hidden Posix functionality of windows.
Thus it is able to join the majority of operating systems out there and
enables to run a platform independent system like Isabelle smoothly.
2- How coul we integrate our tool with Isabelle ?
This important issue got our special attention recently. In the past few
weeks I've been working on a solid wrapper to integrate the Isabelle
process into the JVM environment, enabling to communicate with the Isar
(or ML) toplevel using API calls, instead of fiddling with pipes and
protocols manually. The idea is to make it easy to integrate Isabelle in
JVM based environments out there, such as jEdit or Netbeans, but you can
do anything else with it -- the wrapper not specific to anything.
The other direction is calling other tools from inside Isabelle. People
have occasionally attempted this using the existing Posix process / pipes
/ signals facilities available in SML. Pretty soon we will greatly
improve upon this, by using the internal multithreading facilities of
Poly/ML 5.1, enabling the Isabelle toplevel to speak to several external
tools at the same time (e.g. external provers that potentially diverge.)
If you are interested in any of this, I can point you to some internal
source snapshots. This is still ongoing work, some of it will be part of
the next Isabelle release (this year).
Makarius
Email Gateway (Aug 18 2022 at 11:20):From: Michael Fourman <michael.fourman@ed.ac.uk>
Alessandro,
Poly/ML also has facilities for calling external dynamic libraries -
the "CInterface",
originally implemented by Nick Chapman (then) of Abstract Hardware.
http://www.polyml.org/docs/CInterface.html
This might help you.
In a different context (propplan.sourceforge.net), I use these to call
a BDD library.
Michael
Last updated: May 03 2024 at 12:27 UTC