[English Writing] Good references

Reference

In particular, his calculations suggest, the firn of the Wilkins, Larsen C, George VI and Cosgrove shelves in west Antarctica will be saturated with meltwater by the end of the century—a finding which echoes that of a study led by Jan van Angelen, also of Utrecht University, that was published last year in Geophysical Research Letters. [P67, The Economist (Feb 07, 2014)]

This, as they reported in December’s Nature Geoscience, contains some 140 bil- lion tonnes of liquid water. [P67, The Economist (Feb 07, 2014)]

Further explanation or description

Parenthesis

There is, for example, little Neanderthal DNA on the X chromosome (which, along with the Y chromosome, determines an individual’s sex). [P66, The Economist (Feb 07, 2014)]

Dr Forster and his colleagues think the aquifer they have found covers an area of 70,000 square kilometres (about the size of Ireland). [P67, The Economist (Feb 07, 2014)]

em dash (—)

For instance, genes affecting the production of keratin—an important component of hair and skin—showed more Neanderthal influence than most. [P66, The Economist (Feb 07, 2014)]

This would not matter as a one-off, but if it happened repeatedly as new firn formed the consequences could be serious—particularly if, in escaping, it caused more hydrofracturing or acted as a lubricant that encouraged previously stable ice to slip from its bed- rock into the sea. [P67, The Economist (Feb 07, 2014)]

How likely that sort of thing is to happen—and thus how much of a threat firn really is—has yet to be determined. [P67, The Economist (Feb 07, 2014)]

Enumerate

And two studies, one just published in Nature, and one in Science, have now looked in detail at this miscegenation, and tried to understand its consequences. [P66, The Economist (Feb 07, 2014)]

Emphasise

But the fact that so little is known about it emphasises a wider point. [P67, The Economist (Feb 07, 2014)]

Misc

Crucially, though the amount of Neanderthal DNA in any individual is small, the exact bits vary a lot from person to person. [P67, The Economist (Feb 07, 2014)]

Technically, Neanderthals may be gone. But their DNA ghosts linger on. [P67, The Economist (Feb 07, 2014)]

[Latex] A couple of tips about table

Table

Change the vertical space between caption and table

• Include caption package
• Use captionsetup

    \usepackage{caption}
    \captionsetup[table]{skip=10pt} % set the vertical space between caption and table

Change the space between rows in table

• Define a newcommand \ra

    \newcommand{\ra}[1]{\renewcommand{\arraystretch}{#1}} % more space between rows in table

• Use it in the beginning of the table

    \begin{table}[!hbpt]
        \caption{Example} \label{tab:exam}
        \centering
        \ra{1.3}
        \begin{tabular}{@{}lll@{}} %@{} remove the space to the vertical edge
        \end{tabular}
    \end{table}

• For longtable, put it before \begin{longtable}

    \ra{1.4}
    \begin{longtable}[t]{@{}p{2cm}p{1cm}p{2.5cm}p{3cm}p{6.5cm}@{}}

Customize line width of tables

• Include booktabs package

    \usepackage{booktabs} %table rules \toprule, \midrule, and \bottomrule

• \toprule replaces first \hline
• \bottomrule replaces last \hline
• \midrule replaces other \hline
• \cmidrule{2-3} replace \cline
• Change default line width by, such as \toprule[1pt]

Example

\begin{tabular}{@{}lll@{}} %@{} remove the space to the vertical edge
    \toprule[1pt]
    Progression & Due Date & Status\\
    \midrule
    Submit & 30 Sep 2016 & WIP \\ \cmidrule{2-3}
    \bottomrule
\end{tabular}

Multi-pages and long table

• Include longtable package

Example

    \begin{longtable}[]{@{}p{0.7in}p{1.0in}p{1.5in}p{2.7in}@{}}
        \caption{$\Phi$ translation rules} \label{tab:phi_rule} \\
        \toprule
        & & & \\
        \midrule
        & & & \\
        \bottomrule
    \end{longtable}

Multi columns

• Use \multicolumn

Example

    \midrule
     & \multicolumn{3}{p{5.5in}}{In order to identify the state space.} \\ \cmidrule{2-4}
    \midrule

Multi rows

• Include multirow package

    \usepackage{multirow} %\multirow

• Use \multirow command

Example

    \begin{tabular}{@{}p{1cm}p{4cm}p{2.8cm}p{0.7cm}p{5cm}@{}}
        \toprule
        Stage & Description & Deliverables & Status & Notes \\
        \midrule
        \multirow{2}{*}{Stage1} & \multirow{2}{*}{\parbox{4cm}{approach}} & Conference Paper & Done & \\
        & & Simple Translator & Done & Simple translator is ready \\
        \bottomrule
    \end{tabular}

Remove the space to the vertical edge

• @{} remove the space to the vertical edge

For example

• Remove left and right vertical edge

    \begin{tabular}{@{}p{1cm}p{4cm}p{2.8cm}p{0.7cm}p{5cm}@{}}

Text wrap in table cell

by p{} column specification

• such as

    \begin{tabular}{@{}p{1cm}p{4cm}p{2.8cm}p{0.7cm}p{5cm}@{}}
        & & Simple Translator & Done & Simple translator is ready \\
        & & Simple \newline Translator & Done & Simple translator is ready \\

• \newline command can be used to break the line

by \parbox{}

• such as

    {\parbox{5.0in}{Some of expressions, operators and predicatesle}}

Change the Windows PATH environment variable

1. Can not edit the environment variable by system setting due to access right
Go to "Control Panel" => "System" => "Advanced System Setting", it is denied because my user doesn't have the right to edit it.

2. Change it by SETX command

C:\> setx PATH "%PATH%;d:\cygwin\;c:\python27"

3. Then open another command prompt, and use the set command to check

C:\>set PATH
Path=C:\Perl64\site\bin;C:\Perl64\bin;C:\Program Files (x86)\MiKTeX 2.9\miktex/b
in;C:\Windows\system32;C:\Windows;C:\Windows\System32\Wbem;d:\cygwin;c:\python27"

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.