Event-B Theories: Difference between revisions

(Created page with 'ProB has (limited) support for theories. Currently supported are (examples refer to the theory project below): * recursive datatypes (e.g. the List datatype) * operators defined…')
 
 
(16 intermediate revisions by 2 users not shown)
Line 4: Line 4:
* recursive datatypes (e.g. the List datatype)
* recursive datatypes (e.g. the List datatype)
* operators defined by direct definitions (e.g. operators in the BoolOps theory) or recursive definitions (e.g. operators in the List theory)
* operators defined by direct definitions (e.g. operators in the BoolOps theory) or recursive definitions (e.g. operators in the List theory)
* special annotated operators (see below)
* special annotated operators like transitive closure (see below)


Axiomatically defined operators are not supported without additional annotations.
Axiomatically defined operators are not supported without additional annotations.
Line 12: Line 12:
An example project with theories: [[media:theories2.zip]]
An example project with theories: [[media:theories2.zip]]


'''TODO''': A description of the supported parts.
The project contains the following theories:
; SUMandPRODUCT
: Contains two operators SUM and PRODUCT which take a set of the type POW(T**INT) as argument (with T being a type variable) and return the sum (resp.) product of all element's integer value.
The operators are annotated such that ProB uses an extra implementation.
; Seq
: The theory of sequences provides operators for sequences that are defined by direct definitions, thus supported by ProB.
; Real (unsupported)
: A theory of real numbers, currently unsupported by ProB.
; Natural
: A theory of inductive naturals (defined by a constant zero and a successor function).
: The mkinat operator is annotated such that ProB uses an explicit implementation.
; List
: A theory of lists that are either empty or have a head and a tail
; FixPoint (not really supported)
: The theory is defined by direct definitions but they usually get so complex that ProB cannot cope with them.
; closure
: The operator for transitive closure is supported by ProB.
: The operator is annotated such that ProB uses the classical B implementation.
; Card (contains no operators or data types)
: Contains theorem about set cardinalities.
; BoolOps
: Operators on Booleans (e.g. AND, OR) are defined by direct definitions and as such supported by ProB.
; BinaryTree
: Binary Trees are supported by ProB.


== Tagging operators ==
== Tagging operators ==
<div style="background-color:yellow;border-width:thin;border-style:dashed;padding:5pt">'''Please note:''' The use of these tags is for experts only. Normally such annotations are delivered with a theory. If you think ProB should provide specific support for a theory, please contact us.
</div>


ProB has some extra support for certain operators. ProB expects an annotation to an operator that provides the information that it should use a specific implementation for an operator.
ProB has some extra support for certain operators. ProB expects an annotation to an operator that provides the information that it should use a specific implementation for an operator.
Line 23: Line 49:
where '''Name''' is the name of the operator in the theory and '''Tag''' is a ProB internal name.
where '''Name''' is the name of the operator in the theory and '''Tag''' is a ProB internal name.


The use of these tags is usually for experts only. In the theory file below, some of the theories are annotated.
Currently are the following tags supported (with T being an arbitrary type):
 
{| class="wikitable"  
Currently are the following tags supported:
! Tag      || Description                                               || Expected type || Return type
{| class="wikitable"
! Tag      || Description           || Expected type
|-
|-
| closure1 || the transitive closure || POW(T**T)
| closure1 || the transitive closure                                     || POW(T**T)    || POW(T**T)
|-
|-
| SIGMA    || the sum of a set       || POW(T**INT)
| SIGMA    || the sum of a set                                           || POW(T**INT)   || INT
|-
|-
| PI      || the product of a set   || POW(T**INT)
| PI      || the product of a set                                       || POW(T**INT)   || INT
|-
|-
| mu
| mu       || returns the element of a singleton set                    || POW(T)        || T
|-
|-
| choose
| choose   || returns (deterministically) one element of a non-emtpy set || POW(T)        || T
|-
|-
| mkinat(op1,op2)
| mkinat(zero,succ) || returns an inductive natural number where zero and succ are the two operators of a natural number datatype with zero having no args and succ having one arg (an inductive natural)  || INT          || Inductive Nat
|}
|}
'''TODO''': to be continued...
 
As of version 1.12 (mid-september 2022) ProB also transparently accepts <tt>POW(INT)</tt> as type for SIGMA and PI.
It now also accepts many of its [[External_Functions|external functions]] as tag names, such as the
the functions from LibraryStrings.def or LibraryReals.def.
For example, here we map the operator plus to ProB's external function RADD for adding two reals:
<pre>
operator "plus" internal {RADD}
</pre>
 
If you set the preference <tt> AUTO_DETECT_THEORY_MAPPING</tt> to TRUE then ProB will work with several standard Rodin theories even without a .ptm file in the workspace.
 
As of version 1.13 (November 2023) ProB also accepts literals as well as formulas between dollars
in the .ptm files.
For example, here the operator Rone is defined by the literal 1.0 and the operator RRealPlus by an expression (a set comprehension of the positive reals annotated with the symbolic pragma):
<pre>
operator "Rone" internal {1.0}
operator "RRealPlus" internal {$/*@symbolic*/ {x|x:REAL & x>= 0.0}$}
</pre>
 
 
 
=== Error Messages ===
 
In case the <b>.ptm</b> file is missing, you will get an error message such as the following one:
Axiomatic defined operator "SUM" not recognized.
 
=== Examples ===
For reference, here are the contents of some of the <b>.ptm</b> files.
In case of an error message, you can copy these files into your Theory Projects (e.g., using Drag & Drop) and then refresh (F5). After that animation with ProB should work.
* SUMandPRODUCT.ptm
<pre>
operator "SUM" internal {SIGMA}
operator "PRODUCT" internal {PI}
</pre>
* closure.ptm
<pre>
operator "cls" internal {closure1}
</pre>
* Natural.ptm
<pre>
operator "mk_iNAT" internal {mkinat}
</pre>
 
Here are the contents for a Reals theory by Guillaume Dupont:
<pre>
operator "RReal" internal {REAL}
operator "Rone" internal {1.0}
operator "Rzero" internal {zero}
operator "Rtwo" internal {two}
operator "plus" internal {RADD}
operator "times" internal {RMUL}
operator "minus" internal {RSUB}
operator "lt" internal {RLT}
operator "leq" internal {RLEQ}
operator "gt" internal {RGT}
operator "geq" internal {RGEQ}
operator "uminus" internal {RSUB}
operator "inverse" internal {RINV}
operator "divide" internal {RDIV}
operator "abs" internal {RABS}
operator "sqrt" internal {RSQRT}
operator "Rmax" internal {RMAXIMUM}
operator "Rmin" internal {RMINIMUM}
operator "RRealPlus" internal {$/*@symbolic*/ {x|x:REAL & x>= 0.0}$}
operator "RRealMinus" internal {$/*@symbolic*/ {x|x:REAL & x<= 0.0}$}
operator "RRealStar" internal {$/*@symbolic*/ {x|x:REAL & x /= 0.0}$}
operator "RRealPlusStar" internal {$/*@symbolic*/ {x|x:REAL & x> 0.0}$}
operator "RRealMinusStar" internal {$/*@symbolic*/ {x|x:REAL & x< 0.0}$}
</pre>

Latest revision as of 14:28, 18 December 2023

ProB has (limited) support for theories.

Currently supported are (examples refer to the theory project below):

  • recursive datatypes (e.g. the List datatype)
  • operators defined by direct definitions (e.g. operators in the BoolOps theory) or recursive definitions (e.g. operators in the List theory)
  • special annotated operators like transitive closure (see below)

Axiomatically defined operators are not supported without additional annotations.

Download Theories

An example project with theories: media:theories2.zip

The project contains the following theories:

SUMandPRODUCT
Contains two operators SUM and PRODUCT which take a set of the type POW(T**INT) as argument (with T being a type variable) and return the sum (resp.) product of all element's integer value.

The operators are annotated such that ProB uses an extra implementation.

Seq
The theory of sequences provides operators for sequences that are defined by direct definitions, thus supported by ProB.
Real (unsupported)
A theory of real numbers, currently unsupported by ProB.
Natural
A theory of inductive naturals (defined by a constant zero and a successor function).
The mkinat operator is annotated such that ProB uses an explicit implementation.
List
A theory of lists that are either empty or have a head and a tail
FixPoint (not really supported)
The theory is defined by direct definitions but they usually get so complex that ProB cannot cope with them.
closure
The operator for transitive closure is supported by ProB.
The operator is annotated such that ProB uses the classical B implementation.
Card (contains no operators or data types)
Contains theorem about set cardinalities.
BoolOps
Operators on Booleans (e.g. AND, OR) are defined by direct definitions and as such supported by ProB.
BinaryTree
Binary Trees are supported by ProB.

Tagging operators

Please note: The use of these tags is for experts only. Normally such annotations are delivered with a theory. If you think ProB should provide specific support for a theory, please contact us.

ProB has some extra support for certain operators. ProB expects an annotation to an operator that provides the information that it should use a specific implementation for an operator. Such tags are given in a .ptm file (ProB Theory Mapping). The file must have the same name as the theory.

For each annotated operator, the file contains a line of the form

operator Name internal {Tag}

where Name is the name of the operator in the theory and Tag is a ProB internal name.

Currently are the following tags supported (with T being an arbitrary type):

Tag Description Expected type Return type
closure1 the transitive closure POW(T**T) POW(T**T)
SIGMA the sum of a set POW(T**INT) INT
PI the product of a set POW(T**INT) INT
mu returns the element of a singleton set POW(T) T
choose returns (deterministically) one element of a non-emtpy set POW(T) T
mkinat(zero,succ) returns an inductive natural number where zero and succ are the two operators of a natural number datatype with zero having no args and succ having one arg (an inductive natural) INT Inductive Nat

As of version 1.12 (mid-september 2022) ProB also transparently accepts POW(INT) as type for SIGMA and PI. It now also accepts many of its external functions as tag names, such as the the functions from LibraryStrings.def or LibraryReals.def. For example, here we map the operator plus to ProB's external function RADD for adding two reals:

operator "plus" internal {RADD}

If you set the preference AUTO_DETECT_THEORY_MAPPING to TRUE then ProB will work with several standard Rodin theories even without a .ptm file in the workspace.

As of version 1.13 (November 2023) ProB also accepts literals as well as formulas between dollars in the .ptm files. For example, here the operator Rone is defined by the literal 1.0 and the operator RRealPlus by an expression (a set comprehension of the positive reals annotated with the symbolic pragma):

operator "Rone" internal {1.0}
operator "RRealPlus" internal {$/*@symbolic*/ {x|x:REAL & x>= 0.0}$}


Error Messages

In case the .ptm file is missing, you will get an error message such as the following one:

Axiomatic defined operator "SUM" not recognized. 

Examples

For reference, here are the contents of some of the .ptm files. In case of an error message, you can copy these files into your Theory Projects (e.g., using Drag & Drop) and then refresh (F5). After that animation with ProB should work.

  • SUMandPRODUCT.ptm
operator "SUM" internal {SIGMA}
operator "PRODUCT" internal {PI}
  • closure.ptm
operator "cls" internal {closure1}
  • Natural.ptm
operator "mk_iNAT" internal {mkinat}

Here are the contents for a Reals theory by Guillaume Dupont:

operator "RReal" internal {REAL}
operator "Rone" internal {1.0}
operator "Rzero" internal {zero}
operator "Rtwo" internal {two}
operator "plus" internal {RADD}
operator "times" internal {RMUL}
operator "minus" internal {RSUB}
operator "lt" internal {RLT}
operator "leq" internal {RLEQ}
operator "gt" internal {RGT}
operator "geq" internal {RGEQ}
operator "uminus" internal {RSUB}
operator "inverse" internal {RINV}
operator "divide" internal {RDIV}
operator "abs" internal {RABS}
operator "sqrt" internal {RSQRT}
operator "Rmax" internal {RMAXIMUM}
operator "Rmin" internal {RMINIMUM}
operator "RRealPlus" internal {$/*@symbolic*/ {x|x:REAL & x>= 0.0}$}
operator "RRealMinus" internal {$/*@symbolic*/ {x|x:REAL & x<= 0.0}$}
operator "RRealStar" internal {$/*@symbolic*/ {x|x:REAL & x /= 0.0}$}
operator "RRealPlusStar" internal {$/*@symbolic*/ {x|x:REAL & x> 0.0}$}
operator "RRealMinusStar" internal {$/*@symbolic*/ {x|x:REAL & x< 0.0}$}