(2 intermediate revisions by the same user not shown) | |||

Line 69: | Line 69: | ||

It now also accepts many of its [[External_Functions|external functions]] as tag names, such as the | 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. | 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> | |||

Line 76: | Line 91: | ||

Axiomatic defined operator "SUM" not recognized. | Axiomatic defined operator "SUM" not recognized. | ||

=== Examples === | |||

For reference, here are the contents of some of the <b>.ptm</b> files. | 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. | 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. | ||

Line 90: | Line 106: | ||

<pre> | <pre> | ||

operator "mk_iNAT" internal {mkinat} | 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> | </pre> |

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.

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.

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 (**P**roB **T**heory **M**apping). The file must have the same name as the theory.

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

operatorNameinternal {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}$}

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

Axiomatic defined operator "SUM" not recognized.

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}$}