ProB for Rodin should support theorems in guards
Description
Environment
Gliffy Diagrams
Activity
Jenkins Build Server July 16, 2013 at 8:11 AM
SUCCESS: Integrated in
ProB_Tests_Linux64 #6808
support theorem in guards in evaluation view + when loading proof info () (leuschel: rev 7ca66b70f53098ae5790099ead6a1abadbf7728e)
src/bvisual2.pl
src/bmachine.pl
Jenkins Build Server April 18, 2013 at 8:00 PM
Integrated in
ProB_Tests_Linux32 #133
support theorem in guards in evaluation view + when loading proof info () (Revision 7ca66b70f53098ae5790099ead6a1abadbf7728e)
Result = SUCCESS
leuschel :
Files :
src/bvisual2.pl
src/bmachine.pl
Jenkins Build Server April 18, 2013 at 7:49 PM
Integrated in
ProB_Tests_Leopard64 #125
support theorem in guards in evaluation view + when loading proof info () (Revision 7ca66b70f53098ae5790099ead6a1abadbf7728e)
Result = SUCCESS
leuschel :
Files :
src/bmachine.pl
src/bvisual2.pl
Jenkins Build Server April 18, 2013 at 6:41 PM
Integrated in
ProB_Tests_Windows #331
support theorem in guards in evaluation view + when loading proof info () (Revision 7ca66b70f53098ae5790099ead6a1abadbf7728e)
Result = SUCCESS
leuschel :
Files :
src/bmachine.pl
src/bvisual2.pl
Michael Leuschel April 18, 2013 at 10:07 AM
theorems (in guards) now appears in the ProB for Rodin state view and the ProB Tcl/Tk Evaluation view
Details
Details
Assignee
Michael LeuschelReporter
Michael LeuschelPriority
Major
theorems in guards are currently ignored.
They should be at least shown in the State view under the "guards" section.
We should also examine whether they should be used for multi-level refinement and or cbc-refinement checking.
Below is a minimal example (Camille syntax).
machine ThmInGuard
variables x
invariants
@inv1 x ∈ ℤ
events
event INITIALISATION
then
@act1 x ≔ 0
end
event inc
where
@grd1 x∈ℕ
theorem @grd2 x≥0
then
@act1 x ≔ x + 1
end
end