[English] indefinite vs. definite articles

Articles are so difficult for me. It is inevitable to make mistake when writing a research paper. It is also a problem always mentioned by reviewers, including my supervisor as well. It is so bad!

Besides, I also took a test from British Council. The result is no surprise. Only 7 in 12 are right.

Below is a summary from references for a/an and the articles.

Reasons to use the indefinite (a/an) article before a noun

• countable nouns but doesn’t know exactly which one
  • I would like an apple.
• one of a group
  • I am a student in the university.
• a job or position
  • I am a software engineer.
• all things of the kind
  • A computer has a CPU. (All computers have a CPU.)

Reasons to use without articles before a noun

• plural nouns
  • Many softwares are developed to increase the productivity at work.
• uncountable nouns
  • Information can be encoded into different formats in a computer.
  • Life is harder today than …
• continents
  • Africa, Asia, North America, South America, Antarctica, Europe and Australia
• languages
  • Chinese, English, French etc
  • She is fluent in French.
• specific year
  • She was born in 1989.

Reasons to use the definite article before a noun

• only one
  • The earth/the sun/the moon
• before superlative adjective
  • She is the most beautiful girl in our class.
  • She is the best person I ever met.
• only one in that place
  • The button on the right window is blue.
• already mention it
  • This work presents a new approach to address the model checking issue. The approach is …
• all things referred by a noun
  • The elephant is really a big animal. (Elephants are really big animals.)
• musical instruments
  • I can play the piano.
  • The guitar is a popular musical instrument.
• refer to a system or service
  • The police is on the way.
  • I am listening to the radio.
  • How long does it take by the bus?
• with adjectives to talk about groups of people
  • The poor
  • The rich
  • The elderly
  • The disabled
• no article with names
  • London is a big city.
  • Jane Austen was an English novelist.
  • We are from China.
• names of countries contain Kingdom, States and Republic
  • the United Kingdom
  • the United States
  • the People’s Republic of China
• names of counties are plural
  • the Netherlands, the Philippines
• geographical features
  • the Atlantic, the Arctic Ocean, the West Lake, the Panama Canal, the Himalayas
• newspapers
  • The Times, The Sun, The Daily Mail
• famous buildings or works of art
  • the Taj Mahal, the Great Wall, the Mona Lisa
• organisations
  • the United Nations, the Red Cross
• hotels, pubs and restaurants
  • the Grand Budapest Hotel
  • no article if it’s the owner’s name: Hilton Hotel
• families
  • the Smiths
• decade/era
  • For people born in the 1960’s,

​

[Eiffel] design by contract

This is a very simple example. There are two levels of contract.

• The contract for set_val routine: require states the precondition of this routine that the argument v shall not be negative; ensure enforces the postcondition of this routine that the val shall be equal to v. 
• Class invariant enforces that for all objects/instances of this class their val shall not be negative.

The do  clause actually is an implementation of the specification, expressed by precondition and postcondition, of reset or set_val. If the implementation violates the specification, then bugs are found. This concept is similar to the refinement check in B method. When we regard class in Eiffel as a B machine, member features map to variables in B, create maps to initialisation in B and invariant to invariant. However in B method, a specification and its implementation are in different machine but Eiffel takes them together.

In B method, it can check the correctness between the implementation and the specification by a theorem prover or a model checker. In Eiffel, it might use the hybrid method (static analysis plus test run) to check it.

If we can write the specification in B method (or similar formal languages such as Z notation, VDM), then refine them to an implementation by the refinement check. Afterwards, we may translate this refinement to Eiffel language and also keep the specification. It might be a good way from a formal specification, formal verification and finally to the code.

[Eiffel] first impression

Just read a blog from professor Bertrand Meyer at CACM. For me, it is the second time to hear about Eiffel. I can not recall when to read it before but just have a bit impression of this term.

I also searched my email@University and found some information about it. One is about a seminar from the professor but unfortunately I didn’t participate. And another news is about the honorary doctorate to the professor from my university (University of York) in 2014.

When I was reading the post, I am very interested in the concept of fixing bugs automatically by AutoFix. So took some time (about 4 hours) to read the introductions of Eiffel from Wikipedia and Eiffel Software. And there are some good presentations.

Some key features of Eiffel are shown below.

​

Eiffel Language

• Object-Oriented
  • Inheritance
  • Class
    • Feature
    • Create
    • Invariant
• Design by Contract [Specification]
  • Precondition by "require"
  • Postcondition by "ensure"
  • Class Invariant
    • Inherited
• Static Typing
  • Instead of dynamic typing
  • Typing check before execution and done in compiler
• Void-Safety
  • NullPointer is a nightmare (Java, C, ...)!
  • Protect runtime errors caused by calls to null
  • An attached variable is not allowed to be set to void
• SCOOP
  • Only add one "separate" keyword

Multiple Java versions management and switch on Mac OS X

For my research, I do need at least two different Java versions (6.0 and 7.0 or above) on my Mac OS X. I found this tool jEnv is very useful and the Andrew’s “ Managing multiple versions of Java on OS X” is helpful.

• Check Current Java Version

    $ java -version
    java version "1.6.0_65"
    Java(TM) SE Runtime Environment (build 1.6.0_65-b14-466.1-11M4716)
    Java HotSpot(TM) 64-Bit Server VM (build 20.65-b04-466.1, mixed mode)
    $ /usr/libexec/java_home
    /System/Library/Java/JavaVirtualMachines/1.6.0.jdk/Contents/Home
    $ ls /System/Library/Java/JavaVirtualMachines/
    1.6.0.jdk
  

Installation of jEnv

• Install

    $brew install jenv
  
    ==> Downloading https://homebrew.bintray.com/bottles/jenv-0.4.3.yosemite.bottle.tar.gz
    ######################################################################## 100.0%
    ==> Pouring jenv-0.4.3.yosemite.bottle.tar.gz
    ==> Caveats
    To enable shims and autocompletion add to your profile:
      if which jenv > /dev/null; then eval "$(jenv init -)"; fi
  
    To use Homebrew's directories rather than ~/.jenv add to your profile:
      export JENV_ROOT=/usr/local/opt/jenv
  
    ==> Summary
    🍺  /usr/local/Cellar/jenv/0.4.3: 74 files, 308K 
  

• Follow the instruction

    $ echo 'if which jenv > /dev/null; then eval "$(jenv init -)"; fi' >> .bash_profile
  

• Check

    $ jenv versions
    * system (set by /Users/ykf_2001/.jenv/version)
  

Installation of Java 8

• Download and install it manually from Oracle
• Check it

    $java -version
    java version "1.8.0_45"
    Java(TM) SE Runtime Environment (build 1.8.0_45-b14)
    Java HotSpot(TM) 64-Bit Server VM (build 25.45-b02, mixed mode)
    $ /usr/libexec/java_home
    /Library/Java/JavaVirtualMachines/jdk1.8.0_45.jdk/Contents/Home
    $ ls /Library/Java/JavaVirtualMachines/
    jdk1.8.0_45.jdk
  

• So now the OS comes with Java 8
• List all javas installed

    $ /usr/libexec/java_home -verbose
    Matching Java Virtual Machines (3):
        1.8.0_45, x86_64:    "Java SE 8"    /Library/Java/JavaVirtualMachines/jdk1.8.0_45.jdk/Contents/Home
        1.6.0_65-b14-466.1, x86_64:    "Java SE 6"    /System/Library/Java/JavaVirtualMachines/1.6.0.jdk/Contents/Home
  

Add of old Java 6 and Java 8 to jEnv

    $ jenv add /System/Library/Java/JavaVirtualMachines/1.6.0.jdk/Contents/Home
    oracle64-1.6.0.65 added
    1.6.0.65 added
    1.6 added
    $ jenv versions
    * system (set by /Users/ykf_2001/.jenv/version)
      1.6
      1.6.0.65
      oracle64-1.6.0.65
    $ jenv add /Library/Java/JavaVirtualMachines/jdk1.8.0_45.jdk/Contents/Home/
    oracle64-1.8.0.45 added
    1.8.0.45 added
    1.8 added
    $ jenv versions
    * system (set by /Users/ykf_2001/.jenv/version)
      1.6
      1.6.0.65
      1.8
      1.8.0.45
      oracle64-1.6.0.65
      oracle64-1.8.0.45

Configurations

• Set global Java version to Java 8

    $ jenv global oracle64-1.6.0.65
    $ jenv versions
      system
      1.6
      1.6.0.65
      1.8
      1.8.0.45
    * oracle64-1.6.0.65 (set by /Users/ykf_2001/.jenv/version)
      oracle64-1.8.0.45
    $ jenv global oracle64-1.8.0.45
    $ jenv versions
      system
      1.6
      1.6.0.65
      1.8
      1.8.0.45
      oracle64-1.6.0.65
    * oracle64-1.8.0.45 (set by /Users/ykf_2001/.jenv/version)
    $ cat ~/.jenv/version
    oracle64-1.8.0.45
    $ java -version
    java version "1.8.0_45"
    Java(TM) SE Runtime Environment (build 1.8.0_45-b14)
    Java HotSpot(TM) 64-Bit Server VM (build 25.45-b02, mixed mode)
  

• Set the Java 6 for local directories

    ~/Programs/eclipse-kepler-for-czt$ jenv local oracle64-1.6.0.65
    ~/Programs/eclipse-kepler-for-czt$ jenv versions
      system
      1.6
      1.6.0.65
      1.8
      1.8.0.45
    * oracle64-1.6.0.65 (set by /Users/ykf_2001/Programs/eclipse-kepler-for-czt/.java-version)
      oracle64-1.8.0.45
    ~/Programs/eclipse-kepler-for-czt$ cd ~/Workspace/czt-code-20150622/
    ~/Workspace/czt-code-20150622$ jenv local oracle64-1.6.0.65
    ~/Workspace/czt-code-20150622$ jenv versions
      system
      1.6
      1.6.0.65
      1.8
      1.8.0.45
    * oracle64-1.6.0.65 (set by /Users/ykf_2001/Workspace/czt-code-20150622/.java-version)
      oracle64-1.8.0.45
  

​