Monthly Archives: April 2014

Moving WordPress blog to Azure from Webio hosting

Microsoft Azure

I decided to move my blog from hosting on to Microsoft Azure (formerly Windows Azure before March, 25th 2014). Why? To get more familiar with the Cloud and especially Azure.

I did my migration following Dave Bost’s series Moving a WordPress Blog to Windows Azure:

However, not everything went smoothly and easy. Additionally, I adjusted some steps to my needs/settings/plugins/hosting(Webio).

Small adjustments

Instead of connecting through FTP to copy content (uploads/themes/plugins), I used UpdraftPlus plugin. Moreover, I am using it for weekly backups all the time. It is really nice, especially the cloud backup option, which allows me to put backup files into my Dropbox automatically.

To export my database I used phpMyAdmin provided by Webio. As Portable phpMyAdmin plugin is no longer available, I took advantage of Adminer plugin to import database on Azure. Another option is to install phpMyAdmin on Azure.

I am using iTheme2 template, which allows to export customized settings (iTheme2/import tab). After migration, you can easily import it going to the same place.

I had bunch of themes installed. I was testing/experimenting with them when I started my blog. It took me a while to find a way to remove installed theme. You need to go to Appearance/Themes, click on theme you want to remove and then click delete button in right, bottom corner. I deleted all themes, but my current one (iTheme2) and Twenty-* themes.

WordPress - Delete theme

Webio specific

Specific for any hosting provider is setting the custom domain. In order to do that on Webio, you need to go to Domains/Edit DNS entries (in polish: Domeny/Edytuj wpisy w strefie DNS tej domeny). In the image below, there are DNS entries for my domain. Only highlighted entries matters for redirecting domain to Azure:

Webio DNS settings

When you add domain entries in Azure you need to add www.* entry separately (in my case: and More details can be found here.

Azure - manage custom domains

Remember to create/update web.config file, in order to make your custom domain and permalinks (if you use them) working correctly (as mentioned in part 5 of Dave Bost’s tutorial):

<?xml version="1.0" encoding="utf-8" ?>
				<rule name="Main Rule" stopProcessing="true">
					<match url=".*"/>
					<conditions logicalGrouping="MatchAll">
						<add input="{REQUEST_FILENAME}" matchType="IsFile" negate="true"/>
						<add input="{REQUEST_FILENAME}" matchType="IsDirectory" negate="true"/>
					<action type="Rewrite" url="index.php"/>


When I was trying to set SMTP server to my gmail I received following email from Google, after try to send test email:

Google hijack warning

After following steps in provided link, the issue was fixed. There is one interesting thing: I set region for my website to WestUS. However, Google says: “Location: Spain”. Hmm…

Another issue I had was getting 404 error on .woff file (Crayon Syntax Highlighter plugin font file). I solved it, by modifying web.config file as described here.

I had also problem with Tweet, Like, Google +1 and Share plugin. It dosn’t display buttons on home page. I tried some tricks (deactivate, re-install) to solve it, but I didn’t succeed.


For hosting on I was paying around $20/year (start plan). On Azure, I will need to pay at least $10/month for shared instance (required to have domain, which is $120/year. 6x more expensive! Am I crazy? No. As I stated at the beginning, I want to play with Azure. When I decide I am done with that, I can always go back to or some other hosting.

After one week, my estimated bill is  2,07 €.

FreeRTOS Jump Start

In this semester I am taking Real-Time Systems course. In one of the programming assignments, we had to develop program for embedded device Tiva C Series LaunchPad TM4C123G. It is a low-cost evaluation platform for ARM Cortex-based microcontrollers from Texas Instruments. It is very nice board if you want to start with embedded devices. It cost only $25 on eBay. You can connect it to your computer using USB. Finally, the board has key feature of embedded device for beginners: the LED.

Tiva LaunchPad

A typical process-control system can be divided into four types of components: the process, sensors, actuators, and controller (see Figure below). LED allows you to mock your target actuator. Majority of operations performed by embedded devices is control of the actuators. What is nice about LED: it is cheap and easy to control whether and how it is working.

safety critical loop

Code Composer Studio

As a development environment for Tiva C Series I recommend you Code Composer Studio. It is Eclipse based IDE, which makes development easy. Especially for beginners. Tutorial for installation and running first program on Tiva TM4C123G board using Code Composer Studio can be found here. I recommend to follow the “Single Download” option (download 1GB+ file). More precisely, download and install: “EK-TM4C123GXL-CCS: TivaWare for C Series and Code Composer Studio for the Tiva C Series TM4C123G LaunchPad” available on this website. I wasted a lot of time trying to install it following “Individual Downloads” instructions (download <1MB file). Installer was hanging, when it was downloading files form the Internet and never recovers. In "Single Download" most of files are already downloaded along with the installer.


FreeRTOS is one of the most popular Real Time Operating Systems (RTOS). Additionally, it is free. This is where its name comes from (free + Real Time Operating System = FreeRTOS). The System is written in C language. Thus, we write programs for it in C as well. More details can be found on and wikipedia.

The cool thing about FreeRTOS is that it enables easy modifications of Operating System. You can modify e.g. scheduler.

Once you have Code Composer installed. You need to install TivaWare software (which includes FreeRTOS). It can be found in previously downloaded package (if you were following “Single download” option) in TivaWare/SW-EK-TM4C123GXL-1.1.exe.

Running example programs

The TivaWare software contains examples, which are ready to run. You can find them in the directory, where you installed TivaWare C Series software. In my case (default path) it is: C:\ti\TivaWare_C_Series-1.1\examples.

There is an example project freertos_demo. It makes the LED blinking and allows you to manipulate the colors using buttons (located at the bottom of the board). The project can be found in examples\boards\ek-tm4c123gxl\freertos_demo. It is ready to run. You just need to connect the board to the PC, open the project (import it) in Code Composer Studio and run it in debug mode. Code Composer Studio will automatically port the program into the board.

You can modify the code, and make the LED blinking faster or slower. Colors manipulation is also easy.

Queues and semaphores

FreeRTOS supports multitasking. In the Real-Time systems, communication between different tasks are usually implemented using queues and semaphores. It is also the case in freertos_demo program. Buttons send messages to the LED using queues. Semaphores are use to guard concurrent access to UART.

This tutorial is very good point to start with FreeRTOS. It describes basics, queues, semaphores and more.


Developing code for embedded devices is usually, more complex than for Web or Desktop. Running, even very simple application is more complex, because it requires more steps. You need to configure connection between your computer/OS and specific device. Then you need to setup many settings, which varies almost among every device. The communication with ports is also different and every device has different set of them.

There are no universal installers etc. Every single device require slightly different setup. Sometimes, you need to spend hours to run simple “Hello, World!” application. On the other hand, it is fun to create some system, which do stuff outside of your PC.

If you are interested in embedded devices, check out my other post: BeagleBoard – your personal computer smaller than your wallet.

To get started with FreeRTOS and Tiva C Series: check this tutorial to run first program and FreeRTOS Tutorial to get more details. You can buy Tiva C Series LaunchPad on eBay.

SPARK Ada programming language

Before I joined SAnToS Lab, I heard about Ada programming language only a few times. I thought it is an ancient language, that nobody is using anymore. I assumed, that only reason why somebody may bother are some legacy applications written 30 years ago. I thought that safety-critical and high-assurance systems are developed in C/C++ or even Assembly language.

I was wrong.

Ada programming language

First version of Ada programming language – Ada 83 – was designed to meet the US Department of Defence Requirements formalized in “Steelman” document. Since that time, Ada evolved. There were Ada 95, Ada 2005 and Ada 2012 (released in December 10, 2012). Ada is activelly used in many Real-World projects, e.g. Aviation (Boeing 777’s Software is written in Ada), Railway Transportation, Commercial Rockets, Satellites and even Banking. One of the main goals of Ada is to ensure software correctness and safety. The picture below, shows what is the goal of Ada: prevent the Developer from introducing bugs into system by rich tooling and language properties.

Ada responsibilities

Ada does not use curly braces. The code listing below shows “Hello, World” in Ada:

with Ada.Text_IO; 
use Ada.Text_IO;

procedure Hello is 
  Put_Line ("Hello, world!"); 
end Hello;

Basic constructs

The table below, shows C# code, and equivalent Ada code.

C# Ada
x = 5;
x := 5;
x == 5
x = 5
x != 5
x /= 5
// comment
-- comment
int i = 2;
i : Integer := 2;
if (a &gt; b)  
  Console.WriteLine("Condition met");  
  Console.WriteLine("Condition not met");
if a &gt; b then   
 Put_Line("Condition met");
 Put_Line("Condition not met"); 
end if;
  case 0:     
  case 1:
  case 2:     
case i is   
  when 0 =&gt; Put_Line("zero");   
  when 1 =&gt; Put_Line("one");   
  when 2 =&gt; Put_Line("two");   
  when others =&gt; Put_Line("none");
end case;
for (int i=1; i&lt;=10; ++i)  
  Console.WriteLine("Iteration: ");   
for i in 1 .. 10 loop
  Put_Line("Iteration: ");   
end loop;
while(a != b)  
while a /= b loop   
end loop;
  a := a + 1;   
  exit when a = 10; 
end loop;


The equivalent for C# class – in Ada – is package. It has two files: specification (.ads file) and body (.adb file). It is like header (.h) and implementation (.cpp) files for class definition in C++. Additionally:

  • class variables in C# conforms to ‘global’ variables in Ada package (the name ‘global’ in Ada package means that variable is visible for entire package, not entire application like in C/C++)
  • C# class have methods, which returns value or not (void). In Ada, methods are called subprograms. There are two distinguished types of them: functions (returns something) and procedures (does not return anything).

Here is sample C# class:

class Person  
  public int publicVar;

  private int privateVar;

  void MyMethod(int param)
    // do stuff

  public int MultiplyBy(int param) 	
    return param * 2

And its equivalent package in Ada:

package Person is
  publicVar : Integer; 	

  procedure MyMethod(Param : Integer);   
  function MultiplyBy(Param : Integer) return Integer; 
end Person;
-- person.adb
package body Person is 	
  privateVar : Integer;

  procedure MyMethod(Param : Integer)
    -- do stuff

  function MultiplyBy(Param : Integer)
    Result : Integer;
    Result := Param * 2;
    return Result;
end Person;


SPARK programming language is based on Ada. Thus, it is usually referred as “SPARK Ada”.

SPARK is a programming language and static verification technology designed specifically for the development of high integrity software. First version was designed over 20 years ago. SPARK excludes some Ada constructs (i.e. pointers, dynamic memory allocation or recursion) to make static analysis feasible. Additionally SPARK contains tool-set for Software Verification:

  • Examiner – analyze code and ensures that it conforms to the SPARK language; also verify program to some extent using Verification Conditions (e.g. array index out of range, type range violation, division by zero, numerical overflow etc.)
  • Simplifier – simplify Verification Conditions generated by Examiner
  • Proof Checker – prove the Verification Conditions

Using SPARK, a developer takes a Z specification and performs a stepwise refinement from the specification to SPARK code. For each refinement step a tool is used to produce verification conditions (VC’s), which are mathematical theorems. If the VC’s can be proved then the refinement step will be known to be valid. However if the VC’s cannot be proved then the refinement step may be erroneous.

First version of SPARK (SPARK 83) was based on Ada 83. The second version (SPARK 95) – on Ada 95. Current version – SPARK 2005 – is based on Ada 2005. It is a subset of Ada 2005 with annotations. The annotation language support flow analysis and formal verification. Annotations are encoded in Ada comments (via the prefix --#). It makes every SPARK 2005 program, valid Ada 2005 program. Code listing below shows example SPARK 2005 package specification.

package Odometer
--# own Trip, Total : Integer;
	procedure Zero_Trip;
	--# global out Trip;
	--# derives Trip from ;
	--# post Trip = 0;

	function Read_Trip return Integer;
	--# global in Trip;

	function Read_Total return Integer;
	--# global in Total;

	procedure Inc;
	--# global in out Trip, Total;
	--# derives Trip from Trip &amp; Total from Total;
	--# post Trip = Trip~ + 1 and Total = Total~ + 1;

end Odometer;

It is an interface for simple Odometer. There are 4 subprograms (2 procedures and 2 functions):

  • Zero_Trip procedure – reset Odometer to 0
  • Read_Trip function – returns current distance
  • Read_Total function – returns total distance traveled
  • Inc procedure- increment total and current distance by 1

Annotation global means that subprogram uses some global variable. Postfix in, out or in out means that particular variable is read, write or read and write respectively. Annotation derives says that some variable value depends on other variables. E.g. in procedure Inc variable Trip is dependent on its current value (before procedure call). Annotations pre and post define pre- and postconditions of procedure (only post is present in above example). We can see, that in Zero_Trip procedure postcondition requires that variable Trip is equal to 0. In procedure Inc, postconditions requires that variables Trip and Total are incremented by 1 (‘~‘ is the value of variable before procedure call). Annotation own expose private variables for use in public methods specification.

We can see, that SPARK contracts describe the functionality of particular subprograms. It is like documentation. You can find more about SPARK contracts in Tokeneer Discovery tutorial and SPARK 2005 to SPARK 2014 Mapping Specification.

The most popular IDE for SPARK Ada development is GNAT Programming Studio. There is also Eclipse plugin GNATbench.

The next version, SPARK 2014 (based on Ada 2012) is under development. There is partial tool support (in GNAT Programming Studio), but some language features are still not supported. It is worth to mention, that Ada 2012 contains code contracts. Thus SPARK 2014 is just subset of Ada 2012. There are no additional constructs like annotations in SPARK 2005, because now, contracts are part of the language.

In real-world applications, the embedded critical components are written in SPARK while the non-critical components are written in Ada.


I am working with SPARK Ada for more than 1 year. My (beginner) thoughts are as follows:

  • I don’t like the syntax. It is not developer friendly. You need to do a lot of repetitions, of the same code (e.g. subprograms declaration/definition). Syntax is very verbose, e.g. code blocks starts with begin and ends with end keywords. It means more writing than in case when you use ‘curly braces’ for that.
  • It is very hard to create valid and working SPARK program. There are many rules and limitations (e.g. no dynamic allocation).
  • Quite steep learning curve. Additionally, it is not easy to find some resources like tutorials, books, videos.
  • SPARK Ada IDE – GNAT Programming Studio – is very specific, and different than the most popular IDEs (e.g. Visual Studio or Eclipse). It is also less powerful, in case of e.g. intellisense, key shortcuts or project manipulations.

From my perspective, SPARK is a temporary subset of Ada, chosen for software verification. Once, verification techniques evolves, more features of Ada are getting included in SPARK. Maybe, in some day, there will be no SPARK, but just Ada, and tools will be able to verify (reason about) all its features.

More about Ada you can find at Ada Programming at Wikibooks, AdaCore University (video tutorials) and at website. Good place to start getting familiar with SPARK is Tokeneer Discovery tutorial (SPARK 2005) and SPARK 2014 tutorial. This lecture gives SPARK overview in nutshell. More about SPARK 2014 can be found in SPARK 2014 website, SPARK 2014 Toolset User’s Guide and SPARK 2014 Reference Manual. To go deeper, there is a book SPARK: THE PROVEN APPROACH TO HIGH INTEGRITY SOFTWARE by John Barnes.

Spell check in SublimeText

I am working on my Master Thesis using LaTeX and SublimeText.

Today, I found out that SublimeText allows you to check spelling. To enable spell-check: click F6 or go to View->’Spell Check’.

When spell-check is enabled, it displays red squiggles below the misspelled words. By right click on misspelled word you can correct the misspellings. You can also ignore it for all other occurrences of specific word (useful e.g. for Software Projects names).

SublimeText spell check correct

The spell check is performed based on chosen language/dictionary. You get two English dictionaries (en_US and en_GB) along with SublimeText installation. You can find more dictionaries on github repository: SublimeText / Dictionaries (check readme for installation instructions). To change dictionary: go to View->Dictionary.

SublimeText spell check dictionary

SublimeText is not only lightweight IDE. It can also serve as nice text editor.

I really like SublimeText and if you are not using it so far you should try it! There is nice series of posts Sublime is Sublime. Greg Young describe how to configure and take advantage of SublimeText as .NET developer (from color schemes to run unit tests, through git integration).