Precondition and Guard in Classic B

The differences between Precondition and Guard in B machine.

Precondition

Preconditioned substitution (termination)

• \( P \mid S \) called \( P \) pre \( S \): PRE P THEN S END
  • The operation is only activated when P holds. Otherwise, it may result in an incorrect behaviour.
  • \( [P \mid S]R \Leftrightarrow (P \land [S]R) \)
  • If \( P \) doesn't hold, the operation is not guaranteed to achieve anything, say \( R \), since \( P \land [S]R \) never holds whatever \( R \). This substitution which is not able to establish anything is said to be non-terminating substitution

Guard

Guarded substitution (feasibility)

• \( P \Longrightarrow S \) called \( P \) guards \( S \)
  • \( S \) is performed under the assumption \( P \)
  • \( [ P \Longrightarrow S]R \Leftrightarrow (P \implies [S]R) \)
  • If \( P \) holds, post-condition \( R \) is established. Otherwise, if \( P \) is false, \( [ P \Longrightarrow S] \) can establish anything. It's said to be non-feasible.

Differences

\( P \) doesn't hold

• \( P \mid S \) can not establish anything if \( P \) doesn't hold. When \( P \) doesn't hold, the substitution is said to abort. (Like the divergence in CSP)
• \( P \Longrightarrow S \) can establish anything if \( P \) doesn't hold. When \( P \) doesn't hold, the substitution is not feasible.

Postcondition

• In order to establish the post-condition, \( P \mid S \) must prove \( P \) but \( P \Longrightarrow S \) may assume \( P \).

Substitution

• In \( P \mid S \), \( P \) is assumption, which is a contract between the user of the operations and the machine providing the operations
• In \( P \Longrightarrow S \), \( P \) is condition for the substitution \( S \) to be feasible.
• IF P THEN S END. For example, IF 0 < n THEN n := n - 1 END is equal to if 0 < n then n := n - 1 else n := n end

Example and Demonstration

An example

    MACHINE
       PreGuardTest

    VARIABLES
        n
    INVARIANT
        n: NAT
    INITIALISATION
        n := 0
    OPERATIONS
        inc(i) = PRE
            i: NAT 
        THEN 
            n := n + i 
        END;

        dec0(d) = BEGIN
            n := n - d 
        END;

        dec(d) = PRE
            d: NAT & n >= d
        THEN 
            n := n - d 
        END;

        decp(d) = SELECT    d: NAT & n >= d THEN 
            n := n - d 
        END;

        dec1(d) = BEGIN 
            IF n >= d THEN 
                n := n - d 
            END
        END;

        dec2(d) = BEGIN 
            SELECT n > d THEN 
                n := n - d
        WHEN n = d THEN
            n := n - d
        ELSE
            n := n
            END
        END

    END

Demonstration with ProB

default PRE as SELECT

• Precondition will be treated as guard
• when n=0, call dec1(1) will cause invariant voilented.
• when n=0, dec(1) is not enabled since the precondition doesn't hold. So long as decp(1)
• when n=0, call dec1(1) won't change the value of n since the substitution n := n - d is not feasible since 0 >= 1 is false
• when n=0, dec2 works like dec1

default PRE as SELECT is false

• Precondition will be treated as precondition
• just after initialisation, ProB state window showed
  • inc(-1) will cause Precondition i: NAT violated if we assume the MININT and MAXINT is -1 and 3 separately
  • dec(-1) will cause Precondition d: NAT & n >= d violated
  • dec(1), dec(2) and dec(3) will cause Precondition d: NAT & n >= d violated as well

Proof Obligations

References

• J.-R. Abrial, The B-book: assigning programs to meanings. Cambridge University Press, 2005.
• Ken Robinson, An Introduction to the B Method Preconditions and Guards, 2001

[Latex] Math mode in Verbatim or Verb in math mode

Verb in math mode

• Include
  \usepackage{fancyvrb} % math mode in verbatim
• SaveVerb to define verb text
  \SaveVerb{verbtext}+verb text+
• UseVerb
  \UseVerb{verbtext} within math mode

Examples

\usepackage{fancyvrb} % math mode in verbatim
\SaveVerb{verbtext}+verb text+
\begin{align*}
    \UseVerb{verbtext}
\end{align*}

Color the verbatim

Define new blockcode environment

\DefineVerbatimEnvironment{blockcode}
{Verbatim}
{formatcom=\color{blue}}

Examples

\begin{blockcode}
    text to be colored
\end{blockcode}

Break lines in verb

Include this new package: spverbatim

\usepackage{spverbatim} % break lines at spaces when vs. \verb

Use \spverb

\spverb+\langle \listarg \rangle+

Examples

Math in Verbatim

• TBD

Source Code Syntax Highlight in Blogger

How to enable the source code syntax hightlighter for google blogger

SyntaxHighlighter

• Go to Blogger's template
• Click "Backup/Restore" in the upright of page to backup current template at first
• Then "Edit Template"
• Add the following lines just before the line

Examples

js

int function(int i)
{
    return i;
}

C/C++

int function(int i)
{
    return i;
}

References

• SyntaxHighlighter
• How to configure

[Latex] Cross-Reference and automatically increasing number in table cell

The below commands define two counters: cellcounter and cellcounter1, which are used for two tables seperately.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% New Command for Cross-Reference in Table cell
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcounter{cellcounter} % a new counter
% automatically increase the counter, print the value of counter, and label it for reference
\newcommand{\omegalabel}[1]{\refstepcounter{cellcounter}\arabic{cellcounter}\label{#1}}
% remember to reset before a new start
\newcommand{\cellcounterreset}{\setcounter{cellcounter}{0}} % automatically increase the counter

\newcounter{cellcounter1} % a new counter
% automatically increase the counter, print the value of counter, and label it for reference
\newcommand{\philabel}[1]{\refstepcounter{cellcounter1}\arabic{cellcounter1}\label{#1}}
% remember to reset before a new start
\newcommand{\cellcounter1reset}{\setcounter{cellcounter1}{0}} % automatically increase the counter

In the table cell, we can use it like this way.

\begin{tabular}[]{|p{0.6in}|p{1.0in}|p{1.5in}|p{3.0in}|}       
      \hline
       $\Omega_3$ Rule \omegalabel{omega3:rul_gen1} & \multicolumn{3}{p{5.5in}|}{In order to identify the state space, the initialisation and the operations, Z specification must have a schema named \I{Init} for initialisation and the only one schema included in \I{Init} schema defines the state space. A schema, which includes state schema and its decoration, and is not included by other schema, is treated as an operation.} \\ \cline{2-4}
      \hline

\end{tabular}

In another table, we can use it like this way too.

\begin{tabular}[]{|p{0.6in}|p{1.0in}|p{1.5in}|p{3.0in}|}       
        \hline
        $\Phi$ Rule \philabel{phi:rul_abbr} & $AbbrDef==exp$ & \verb+nametype AbbrDef=+ $\Phi(exp)$ & Abbreviation Definition \\
        \hline

\end{tabular}

Then, we can refer to it by

Rule~\ ref{phi:rul_abbr}
Rule~\ ref{omega3:rul_gen1}

The output will be like.