Tool-supported invariant-based programming

The development of correct programs is a core problem in computer science. Although formal verification methods for establishing correctness with mathematical rigor are available, programmers often find these difficult to put into practice. One hurdle is deriving the loop invariants and proving that the code maintains them. So called correct-by-construction methods aim to alleviate this issue by integrating verification into the programming workflow. Invariant-based programming is a practical correct-by-construction method in which the programmer first establishes the invariant structure, and then incrementally extends the program in steps of adding code and proving after each addition that the code is consistent with the invariants. In this way, the program is kept internally consistent throughout its development, and the construction of the correctness arguments (proofs) becomes an integral part of the programming workflow. A characteristic of the approach is that programs are described as invariant diagrams, a graphical notation similar to the state charts familiar to programmers. Invariant-based programming is a new method that has not been evaluated in large scale studies yet. The most important prerequisite for feasibility on a larger scale is a high degree of automation. The goal of the Socos project has been to build tools to assist the construction and verification of programs using the method. This thesis describes the implementation and evaluation of a prototype tool in the context of the Socos project. The tool supports the drawing of the diagrams, automatic derivation and discharging of verification conditions, and interactive proofs. It is used to develop programs that are correct by construction. The tool consists of a diagrammatic environment connected to a verification condition generator and an existing state-of-the-art theorem prover. Its core is a semantics for translating diagrams into verification conditions, which are sent to the underlying theorem prover. We describe a concrete method for 1) deriving sufficient conditions for total correctness of an invariant diagram; 2) sending the conditions to the theorem prover for simplification; and 3) reporting the results of the simplification to the programmer in a way that is consistent with the invariantbased programming workflow and that allows errors in the program specification to be efficiently detected. The tool uses an efficient automatic proof strategy to prove as many conditions as possible automatically and lets the remaining conditions be proved interactively. The tool is based on the verification system PVS and i uses the SMT (Satisfiability Modulo Theories) solver Yices as a catch-all decision procedure. Conditions that were not discharged automatically may be proved interactively using the PVS proof assistant. The programming workflow is very similar to the process by which a mathematical theory is developed inside a computer supported theorem prover environment such as PVS. The programmer reduces a large verification problem with the aid of the tool into a set of smaller problems (lemmas), and he can substantially improve the degree of proof automation by developing specialized background theories and proof strategies to support the specification and verification of a specific class of programs. We demonstrate this workflow by describing in detail the construction of a verified sorting algorithm. Tool-supported verification often has little to no presence in computer science (CS) curricula. Furthermore, program verification is frequently introduced as an advanced and purely theoretical topic that is not connected to the workflow taught in the early and practically oriented programming courses. Our hypothesis is that verification could be introduced early in the CS education, and that verification tools could be used in the classroom to support the teaching of formal methods. A prototype of Socos has been used in a course at Åbo Akademi University targeted at first and second year undergraduate students. We evaluate the use of Socos in the course as part of a case study carried out in 2007.

Industrial solution business – transition from product to solution offering

The business logic in the manufacturing industry has changed in the 21st century. In the current industrial market, manufacturers are driven to provide more comprehensive offerings that go beyond the traditional product-orientation by providing capacity and availability for their customers. From incidental merchandise, services have become the core of manufacturers’ offerings with long-lasting service agreements over the life-cycles of their products. This change is driven both by the need of providers to grow and gain competitive advantage and by increased customer demand caused by customers’ outsourcing trends. The three key drivers for manufacturers’ service strategies are outsourcing trends, saturation of the installed base, and commoditization in product markets. Thus, manufacturers focus on providing industrial solutions which are delivered through relational processes with customers by using solution-driven business models. In the management of marketing activities, this can be regarded as closer customer relationships, service-dominant business logic, and collaboration in solving customers’ problems. However, there are few studies on comprehensive conceptualizations of a solution offering that include different elements and their roles, especially in the context of capital goods industry. Also the transition process needs further studies in a real life context. This study explores the transition process of an industrial company from product to solution business and, as an aid to managing the solution business, explicates the structure and management of an industrial solution offering. There are two themes, the industrial transition process and industrial solution offering. Regarding the industrial transition process, the aim is to understand the supplier view on the process and its execution and to determine the challenges related to the transition process. The industrial solution offering is discussed by its elements and characteristics, as well as management. Furthermore, a special type of build-own-operate-transfer business model is presented and its suitability in the industrial context analyzed. The study includes findings achieved by qualitative methods and from four case companies. Based on the results, it is tentatively suggested that in the industrial solution business, the transition from product to solution business is not a linear project but an evolving process that varies according to customer needs, which suggests that companies need to possess an ability to develop new business models for different customer needs. The industrial solution offering is dynamic as it evolves in collaboration according to the prevailing and latent customer needs, which suggest restructuring of the organization from a product-centric to a customer-centric one. Furthermore, based on the findings, the concept of industrial solutions is defined as an ongoing relational process to satisfy a customer’s particular business or operational requirements, and the concept of industrial solution offering as an entity comprising the customized goods, services, collaboration, and finance needed to fulfill the industrial solution. Finally, the study offers several managerial implications for industrial managers involved in the transition and management of the solution business and its offering.

Evaluation of novel programs in health counseling – their effectiveness in the oral health of young children, and their acceptance by parents and professionals in public dental service.

Aim and design: To evaluate family-based health counseling for young children, and to study the significance of adding parental self-care or the training of professionals to the programs. The effectiveness and acceptability of the programs were evaluated by comparing two new programs with an earlier one. Subjects and methods: The study was carried out in Vantaa, which was divided into three study areas. The subjects consisted of children born in 2008, particularly fi rstborn children, while children born in 2006 formed the historical control. The fi rst of the new programs emphasized oral hygiene and use of fl uoride, and the second program focused on proper diet and use of xylitol. The main outcome measure was mutansstreptococci (MS) in the dental biofi lm of two-year-olds, and the opinions of parents and dental professionals were evaluated using questionnaires. Results: The programs found wide acceptance among dental professionals. There were no group-related differences found in the MS scores of the two-year-olds. However, all groups combined, father’s advanced level of education and child’s proper use of xylitol were associated with negative MS scores. In the opinion of parents, the oral healthcare guidance at least somewhat met their expectations. Conclusions: The present fi ndings suggest that providing training and support for professionals in health education is important. The addition of parental self-care to supplement programs aimed at young children does not improve the program, although it may improve parental readiness to change their own health habits. Counseling for families might be best carried out through a routine patient-centered program.

Puutuotteen markkinapotentiaalin arvioiminen kansainvälisillä markkinoilla, case Havesa

Tutkielman tavoitteena oli arvioida puutuotteen markkinapotentiaalia Saksassa, Ranskassa ja Hollannissa sekä tuottaa markkinainformaatiota case-yrityksen investointipäätösten pohjaksi. Teoreettista tietoa markkinapotentiaalin arvioimisesta ja kilpailun analysoimisesta sovellettiin tutkittavan tuotteen markkinoiden kartoittamiseksi. Työssä tutkittiin rakentamisessa käytettävien puutuotteiden markkinoihin vaikuttavia trendejä niiden markkinoiden tulevaisuuden kehityksen arvioimiseksi. Kyseessä oli soveltava case-tutkimus, joka toteutettiin kirjoituspöytä- ja haastattelututkimuksen yhdistelmänä. Primaaritutkimus suoritettiin puhelimitse ja henkilökohtaisella haastattelulla. Tutkimusaineistoa arvioitiin kvalitatiivisesti. Tutkimuksen avulla saatiin käsitys kyseisen puutuotteen markkinoiden koosta ja sen markkinoiden kehitykseen vaikuttavista tekijöistä. Tutkimuksessa arvioitiin myös korkean jalostusasteen puutuotteen markkinoijalta vaadittavia ominaisuuksia ja menestystekijöitä.

Conversioni al cattolicesimo a Roma tra Sei e Settecento. La presenza degli scandinavi nell’Ospizio dei Convertendi.

In my PhD dissertation, I have examined a group of people of Scandinavian origin received by Ospizio dei Convertendi. This group has been hitherto largely unknown to historical research. The Ospizio was an institute founded by the Oratorian Congregation in Rome in 1673 to provide religious instruction and material aid to both recent and aspirant converts to Roman Catholicism. My research traces the profile of converts and a typology of motives, examining different factors which influenced the conversion process. I show that the key factors were often of a social rather than a religious nature. Moreover, I have analyzed the hospice in the context of Counter-Reformation charity as well. In terms of numbers, the Scandinavians formed a somewhat marginal yet not insignificant group within the Roman hospice. Out of a total of 2203 guests received between 1673 and 1706, 4.6 % were Scandinavians: 74 Swedes (including Finland and Livonia) and 27 Danes (including Norway). They came from a rigorously Protestant region which reacted to Catholicism with severe legislative measures. Converts to Catholicism risked confiscation of their goods, expulsion or even capital punishment. Since both Sweden and Denmark were practically impenetrable to Catholicism at the time and clandestine missionary attempts often failed before they had even properly started, the Roman Catholic Church shifted its interest towards Northerners arriving in Rome, a preferred destination for young noblemen, artists and migrant craftsmen. The material related to Ospizio dei Convertendi, conserved in the Vatican archives, is a scarcely known yet unusually rich source, not only for the religious history of our continent, but also for social history and the study of migration in early modern Europe. It contains a wealth of information about members of the subordinate classes, of their travels and lives in Europe. The profile delineated in these documents is of individuals who had a wide range of different professions and different aspirations. These documents encompass a vast social spectrum that was highly mobile on a continent which by that time had become pluriconfessional. Therefore, these migrants faced the complex religious reality in their everyday life. The principal corpus of my research consists of two types of manuscript sources created for administrative and in a way also for apologetic purposes of the Roman Catholic Church. My starting point is the Primo registro generale of Ospizio dei Convertendi. This is a volume in which the following information about each guest was registered: name, nationality, city of origin, age, sex, profession, confession professed before converting, date of arrival, departure, abjuration and baptism. Typically, the convert was male, originating from Stockholm or Copenhagen, from 21 to 30 years of age. The biggest occupational groups in descending order were soldiers, noblemen, craftsmen and sailors. Thus the data reflects a multiform reality of interurban and long distance migration, ideals regarding the education of young noblemen and gentry as well as the need of European armies to hire foreign mercenaries in their various campaigns. Against this background the almost total absence of women is hardly surprising: there is only one woman in the material I have studied. The second main source, Nota degl’ospiti ricevuti e spese fatte per essi, sheds more light on the choices of the converts, their motivations and their lives outside Scandinavia before reaching Rome. This narrative material permits an analysis which completes but also goes far beyond the columns of the Institute’s general register. This material consists of reports written by Catholic priests based on an interview conducted upon each guest’s arrival. The material frequently includes information on what the converts would do following their departure from the Institute as well. These sources have a specific narrative form and contain short biographies, list reasons for converting and information about the journey from the North to the Mediterranean - a journey which in many cases took several years. Moreover, they show that certain unorthodox practices such as calling on the saints and pleading for help from them were not uncommon in the Protestant popular religion. The recording of information on conversions from Protestantism to Catholicism reflects both religious and social interest on the part of the receiving institute. The information obtained was used for the purposes of religious teaching, for finding adequate ways of inserting the convert into Italian society so that he could earn a living, and to find effective methods to convert others with a similar cultural and geographical background. The stories recorded were based on interviews with the newly-arrived, information obtained from a travel companion or fellow countrymen, or from written documents the aspirant converts carried with them. These sources illustrate, although sometimes in rather simplified ways, the circumstances and motivations which were relevant to the choice of changing one’s confession. In addition, I have examined petitions addressed to the hospice and other Roman authorities in order to get financial aid. These petitions were written by Italian scrittori, and they contain certain conventions and topoi of presenting the conversion with the purpose of improving the chances of obtaining financial aid. It is through these filters, which may seem initially almost invisible, that the remote voice of the converts reaches us. The results of the analysis are particularly interesting because they disagree with some of the principal conclusions of previous work on the subject. First, earlier research has focused almost exclusively on the conversions of noblemen, and has argued, second, that the Queen Christina of Sweden was the driving force behind their change of confession. The sources examined for this dissertation present a profile of long-distance migrants, many of them members of the subordinate classes, who were looking for ways to make their living in Europe. These people had in many cases left their country of origin several years earlier and not for religious reasons, so, crucially, we are not dealing with confessional migration in these cases. Rather, conversion was a complex process, intricately tied up with strategies of survival, integration and upward social mobility. At the same time, while these components are significant on their own right, they do not necessarily point to the absence of motivations of a more clearly religious nature.

Teaching mathematics and programming : new approaches with empirical evaluation

Programming and mathematics are core areas of computer science (CS) and consequently also important parts of CS education. Introductory instruction in these two topics is, however, not without problems. Studies show that CS students find programming difficult to learn and that teaching mathematical topics to CS novices is challenging. One reason for the latter is the disconnection between mathematics and programming found in many CS curricula, which results in students not seeing the relevance of the subject for their studies. In addition, reports indicate that students' mathematical capability and maturity levels are dropping. The challenges faced when teaching mathematics and programming at CS departments can also be traced back to gaps in students' prior education. In Finland the high school curriculum does not include CS as a subject; instead, focus is on learning to use the computer and its applications as tools. Similarly, many of the mathematics courses emphasize application of formulas, while logic, formalisms and proofs, which are important in CS, are avoided. Consequently, high school graduates are not well prepared for studies in CS. Motivated by these challenges, the goal of the present work is to describe new approaches to teaching mathematics and programming aimed at addressing these issues: Structured derivations is a logic-based approach to teaching mathematics, where formalisms and justifications are made explicit. The aim is to help students become better at communicating their reasoning using mathematical language and logical notation at the same time as they become more confident with formalisms. The Python programming language was originally designed with education in mind, and has a simple syntax compared to many other popular languages. The aim of using it in instruction is to address algorithms and their implementation in a way that allows focus to be put on learning algorithmic thinking and programming instead of on learning a complex syntax. Invariant based programming is a diagrammatic approach to developing programs that are correct by construction. The approach is based on elementary propositional and predicate logic, and makes explicit the underlying mathematical foundations of programming. The aim is also to show how mathematics in general, and logic in particular, can be used to create better programs.

Evolution of Bordetella pertussis post vaccination

Evolution of Bordetella pertussis post vaccination Whooping cough or pertussis is caused by the gram-negative bacterium Bordetella pertussis. It is a highly contiguous disease in the human respiratory tract. Characteristic of pertussis is a paroxysmal cough with whooping sound during gasps of breath after coughing episodes. It is potentially fatal to unvaccinated infants. The best approach to fight pertussis is to vaccinate. Vaccinations against pertussis have been available from the 1940s. Traditionally vaccines were whole-cell pertussis (wP) preparations as part of the combined diphtheria-tetanus-pertussis (DTP) vaccines. More recently acellular pertussis (aP) vaccines have replaced the wP vaccines in many countries. The aP vaccines are less reactogenic and can also be administered to school children and adults. There are several publications reporting variation in the i>B. pertussis virulence factors that are also aP vaccine antigens. This has occurred in the genes coding for pertussis toxin and pertactin about 15 to 30 years after the introduction of pertussis vaccines to immunisation programs. Resurgence of pertussis has also been reported in many countries with high vaccination coverage. In this study the evolution of B. pertussis was investigated in Finland, the United Kingdom, Poland, Serbia, China, Senegal and Kenya. These represent countries with a long history of high vaccination coverage with stable vaccines or changes in the vaccine formulation; countries which established high vaccination coverage late; and countries where vaccinations against pertussis were started late. With bacterial cytotoxicity and cytokine measurements, comparative genomic hybridisation, pulsed-field gel electrophoresis (PFGE), genotyping and serotyping it was found that changes in the vaccine composition can postpone the emergence of antigenic variants. It seems that the change in PFGE profiles and the loss of genetic material in the genome of B. pertussis are similar in most countries and the vaccine-induced immunity is selecting non-vaccine type strains. However, the differences in the formulation of the vaccines, the vaccination programs and in the coverage of pertussis vaccination have affected the speed and timing of these changes.

Puolueiden keskustelutilaisuuksista mediatapahtumiksi. Television vaaliohjelmat ja niihin liittynyt sanomalehtijulkisuus 1960-luvulta 1980-luvulle

Tässä tutkimuksessa tarkastellaan television vaaliohjelmia ja niihin liittynyttä sanomalehtijulkisuutta 1960-luvun alusta 1980-luvun lopulle. Tarkastelun kohteena ovat sekä eduskunta- että presidentinvaalien vaaliohjelmat. Tutkimusaineisto koostuu Yleisradion hallinto- ja ohjelmaneuvostojen pöytäkirjoista, vaaliohjelmien televisiotallenteista sekä vaaliohjelmia käsittelevistä sanomalehtikirjoituksista. Lehtiaineisto on kerätty Helsingin Sanomista, Ilta-Sanomista, Iltalehdestä, Aamulehdestä, Kansan Uutisista, Suomenmaasta sekä Suomen Sosialidemokraatista. Sanomalehtiaineistoa on täydennetty Yleisradion leikearkistoon kerätyillä lehtileikkeillä. Tutkimuksessa on analysoitu toisaalta television vaaliohjelmien kehitystä ja toisaalta vaaliohjelmiin liittynyttä sanomalehtikirjoittelua. Television vaaliohjelmien kehityksen osalta tutkimuksessa on kuvattu, millä tavoin vaaliohjelmia on eri aikoina tehty ja millaisia poliittisia kiistoja niiden tekemiseen on liittynyt. Sanomalehtiaineiston analyysissa on tarkasteltu sitä, mihin seikkoihin vaaliohjelmia käsittelevissä kirjoituksissa on kiinnitetty huomiota, millä tavoin lehdet ovat suhtautuneet ohjelmien toteutukseen ja millainen rooli ohjelmilla on nähty olleen vaalikampanjoinnissa. Väitöskirjan näkökulma on historiallinen, mikä merkitsee ajallisten kontekstien keskeisyyttä analyysissa. Tutkimuksessa on kiinnitetty huomiota sekä poliittisessa kulttuurissa että mediamaisemassa tapahtuneisiin muutoksiin. Vaaliohjelmat olivat 1960-luvulla tarkkaan säänneltyjä puolueiden välisiä keskustelutilaisuuksia, joissa toimittajilla ei ollut näkyvää roolia. Ohjelmien toteutuksesta vastasivat puoluemandaateilla toimineet Yleisradion ohjelma- ja hallintoneuvoston jäsenet, joten ohjelmien toteutuksen yksityiskohdista vastasivat puolueet. Puolueet riitelivät usein vaaliohjelmien toteutuksesta, mikä osoittaa, että puolueille television vaaliohjelmat olivat tärkeitä poliittisia foorumeita jo 1960-luvulta lähtien. Vaaliohjelmat jakautuivat kahteen erilaiseen ohjelmaformaattiin; vaalitentteihin ja suureen vaalikeskusteluun. Vaalitenteissä kunkin puolueen edustajat olivat vuorollaan ”altavastaajina”, joille muiden puolueiden edustajat esittivät kysymyksiä. Suuri vaalikeskustelu oli perinteisempi paneelikeskustelu, jossa poliitikot selvittivät vuorotellen kantojaan ajankohtaisiin poliittisin kysymyksiin. 1970-luvun puolivälissä vaalitenttien toteutuksessa tapahtui suuria muutoksia, kun toimittajat syrjäyttivät poliitikot vaalitenttien kyselijöinä. Suuri vaalikeskustelu säilyi ennallaan. Sanomalehtien suhtautuminen vaaliohjelmiin oli 1960- ja 1970-luvuilla huomattavasti pidättyvämpää kuin poliitikkojen. Sanomalehdistön näkökulmasta television vaaliohjelmien tärkeimpänä tehtävänä oli puolueiden poliittisten linjausten esittely. Vaaliohjelmia käsittelevissä teksteissä esiteltiin pääasiassa poliitikkojen ohjelmissa pitämiä puheenvuoroja. Puoluelehdissä puheenvuorojen sisältöä arvioitiin aatteellisista lähtökohdista, sitoutumattomissa sanomalehdissä neutraalimmin. Vaaliohjelmien toteutukseen liittynyt kritiikki kohdistui toisaalta poliitikkojen puoluepropagandaan, toisaalta poliitikkojen liialliseen varovaisuuteen. Sanomalehtien suhtautuminen vaaliohjelmiin säilyi ennallaan myös 1970-luvulla, jolloin vaaliohjelmia alettiin tehdä toimittajavetoisesti. Ainoa muutos liittyi vaaliohjelmakritiikkiin, joka kohdistui nyt poliitikkojen ohella myös toimittajiin, joiden katsottiin olleen ohjelmissa liian hyökkääviä. Suurin muutos vaaliohjelmiin liittyneessä kirjoittelussa tapahtui 1980-luvulla. Vaaliohjelmia käsitteleviä kirjoituksia julkaistiin sanomalehdistössä monikertainen määrä 1970-lukuun verrattuna. Samalla myös vaaliohjelmia käsittelevien kirjoitusten näkökulmat alkoivat muuttua, kun ohjelmin visuaalinen ulottuvuus alkoi olla yhä näkyvämmin esillä sanomalehtiin laadituissa analyyseissa. Lehdet alkoivat teettää säännöllisesti erilaisia tutkimuksia poliitikkojen pärjäämisestä ohjelmissa ja kirjoittaa vaalikeskusteluiden voittajista ja häviäjistä. Lisäksi lehtijutuissa arvioitiin poliitikkojen esiintymistä ja vaaliohjelmista välittyviä vaikutelmia. Vuoden 1982 presidentinvaaleissa uusista näkökulmista kirjoittivat erityisesti iltapäivälehdet, mutta vuosikymmenen jälkipuoliskolla samankaltaisia lähestymistapoja omaksuivat myös Helsingin Sanomat ja Aamulehti. Niiden vaaliohjelmia käsittelevissä uutisissa kiinnitettiin yhä useammin huomiota poliitikkojen esiintymiseen, pukeutumiseen ja tunnetiloihin. Puoluelehtien suhtautuminen vaaliohjelmiin säilyi kuitenkin ennallaan, ja myös vaaliohjelmakritiikki säilyi suurelta osin muuttumattomana. 1980-luvun aikana television vaaliohjelmat muuttuivat lehdistön käsittelyssä puolueiden tavoitteita esittelevistä keskustelutilaisuuksista poliitikkojen ja puolue johtajien henkilökohtaisia ominaisuuksia mittaaviksi esiintymiskokeiksi ja suuriksi mediatapahtumiksi, joiden katsottiin toisinaan jopa ratkaisseen vaalin tuloksen. Nostaessaan television vaaliohjelmat kampanjajournalisminsa ytimeen, sanomalehdet vahvistivat television poliittista roolia.

Acquisition Failure: The case of a multinational enterprise from an emerging market failing in Indonesia.

The escalation in the number of mergers and acquisition transactions involving emerging market firms is a relatively recent phenomenon; as a consequence academic research in such topic is rather limited. The purpose of this research study was to discuss the possible reasons that led the acquisition failure of an emerging multinational firm and an Indonesian player. Extensive theoretical research was performed and it had been achieved, based on this, the finding of a framework that facilitated to understand the way in which the concepts of cultural distances and relate liabilities of foreignness in the process of acquisitions of foreign companies in emerging markets. The theoretical background collects literature related to acquisitions, models of cultural studies between nations and liabilities of foreignness. It has been generated a variety of frameworks that aid to understand the way that the institutional distance and cultural factors together with the concept of liabilities of foreignness can affect the process of market entry of an emerging multinational company to the extent that the best way to stop losing money is to abandon the project. The empirical research consisted of selective semi-structured interviews and an extensive research in available public data on the chosen study case of this research. There were several factors that were identified as the cause of the failure in the market entry of a Mexican multinational firm in Indonesia. The weakness shown by the local government authorities was used by the local community leaders who rioted because of discomfort. These groups were the ones who made the government submit to the extent that the agreements reached at the beginning of the deal were either canceled or modified in a way that favored always the local community. The contributions of this study fall into the knowledge field of emerging multinational firms and market entry process.