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.

Tulevaisuuden lähtökohdista kansanvallan kolmiliittoon. Kansallinen Edistyspuolue ja kansallisen eheytymisen politiikka 1919–1939.

Kansallista Edistyspuoluetta ja sen toimijoita maailmansotien välisen Suomen sisäpolitiikassa tarkasteleva väitöstutkimus paneutuu puolueen kansallista eheytymistä ajaneen poliittisen linjan taustoihin, muodostumiseen ja toteutumiseen maailmansotien välisenä aikana vuosina 1919-1939. Vahvasti aineistopohjainen ja lähdekriittinen poliittisen historian tutkimus keskittyy parlamentaarisiin toimijoihin, poliittiseen kenttään ja näiden tuottamiin aineistoihin, kuten edistyspuolueen ja sen toimijoiden arkistoihin, lehdistöön ja valtiopäiväpöytäkirjoihin. Tutkimus selvittää, millainen oli edistyspuolueen kansallisen eheytymisen linja, mihin sillä pyrittiin, miten sitä toteutettiin ja miten se toteutui. Kansainvälisen vertailun kautta tutkimuksessa luodaan myös kuva suomalaisesta liberalismista ja liberalistista. Joulukuussa 1918 perustettu Kansallinen Edistyspuolue oli liberaali puolue, jonka politiikassa korostui erityisesti liberalismin sosiaalinen tulkinta. Puolueen sisäpoliittiseksi linjaksi vastaitsenäistyneessä ja sisällissodan runtelemassa valtiossa muodostui kansallisen eheytymisen edistäminen. Ajatuksen taustalla olivat K. J. Ståhlbergin tulevaisuuden lähtökohtia hahmotelleet artikkelit, jotka julkaistiin Helsingin Sanomissa huhtikuussa 1918 sisällissodan vielä riehuessa. Ståhlbergin mukaan kansalliseen eheytymiseen ei tullut pyrkiä sodan vuoksi vaan siitä huolimatta. Nuorsuomalaiselta puolueelta perityt liberaalit periaatteet täydentyivätkin edistyspuoluelaisessa ajattelussa sisällissodan ja tasavallan puolesta käydyn valtiomuototaistelun avainkokemuksilla. Itsenäisen Suomen ensimmäisiä vuosia hallinneissa keskustahallituksissa kansallista eheytymistä edistettiin sosiaalipoliittisin uudistuksin mm. oppivelvollisuus- ja asutuslakien muodossa. Myös sisällissodan vankien armahdukset olivat osa tätä ohjelmaa. Tutkimus osoittaa, että edistyspuolueen kansallisen eheytymisen politiikan keskeisenä tavoitteena oli poliittisen sovittelun kautta integroida vasemmisto osaksi parlamentaaris-demokraattista järjestelmää. Eheytyspolitiikan todellinen käyttöarvo ja edistyspuolueen poliittiset toimintamahdollisuudet alkoivat kuitenkin heiketä vuoden 1922 eduskuntavaalien jälkeen.Tutkimuksesta käy ilmi, että toteutettu eheytyspolitiikka ja sen osittainen epäonnistuminen näkyivät sekä kommunistien jatkuvana kannatuksena että sisäpoliittisen ilmapiirin oikeistolaistumisena. Tämä kehitys nosti myös edistyspuolueessa esille voimat, jotka suosivat porvariyhteistyötä ohi keskustavasemmistolaisen eheytyspoliittisen linjan. Alkuvuosien jälkeen valtiomuototaistelun koossapitävä voima heikkeni edistyspuolueen sisällä ja 1920-luvun puolivälissä käydyt linjakiistat osoittivat, että osalle puolueen jäsenistä vuoden 1918 puoluevalinnassa keskeisemmässä roolissa oli ollut tasavaltalaisuus kuin vasemmiston integrointi ja kansallinen eheytyminen. Edistyspuolueen johto ei kuitenkaan ollut valmis luopumaan eheytyspoliittisesta linjasta ja sen ympärille luodusta puolueidentiteetistä, joten porvariyhteistyötä kannattanut oikeisto-oppositio päätyi suurelta osin eroamaan puolueesta vuonna 1927. Tutkimus osoittaa, että parlamentarismin rapautuminen ja pienelle yleispuolueelle elintärkeiden yhteistyömahdollisuuksien heikkeneminen luokkapuolueiden puristuksessa johtivat edistyspuolueen kannatuksen alamäkeen sotien välisenä aikana. Se kutistui 26 kansanedustajan keskisuuresta puolueesta vain kuuden edustajan pienpuolueeksi. Puolueidentiteetin vahvuus ja keskeisten toimijoiden puolueen kokoa suurempi poliittinen painoarvo pitivät sen lakkauttamispohdinnoista huolimatta kuitenkin koossa ja kiinni politiikan ytimessä. Oikeistoradikalismin vuodet 1920–1930-lukujen taitteessa olivat edistyspuolueellesekä uhka että mahdollisuus. Tutkimuksessa käy ilmi, että vaikka kommunisminvastaisen kansanliikkeen vaatimukset olivat edistyspuoluelaisten mielestä oikeutettuja, oli kansanliikkeen niiden ajamiseksi omaksumia laittomia ja ulkoparlamentaarisia keinoja vaikea hyväksyä. Eheytyspolitiikan kannalta katsottuna melkotoivottamalta näyttänyt tilanne kääntyi kuitenkin lopulta voitoksi: äärivasemmisto eliminoitiin, äärioikeisto ajautui paitsioon ja tie maltillisen vasemmiston ja keskustan yhteistyölle aukesi jälleen. Tämä johti lopulta vuonna 1937 punamultahallitukseen ja kansanvallan kolmiliittoon Kansallisen Edistyspuolueen, SDP:n ja Maalaisliiton kesken. Kokemus siitä, että itsenäisyys oli alati uhattuna, toi suomalaiseen liberalismiin varsin nationalistisia piirteitä, joita eurooppalaisten veljespuolueiden ohjelmista ei löydy. Liberalismiin usein liitetty mielleyhtymä sen kosmopoliittisesta, kansallisvaltioita ylittävästä luonteesta jäi Suomessa sotien välisenä aikana nationalismin ja itäisen naapurin luoman uhan varjoon. Suomen sisäpoliittinen tilanne ja geopoliittinen asema loivat vaatimuksen vahvasta kansallisesta yhtenäisyydestä. Suomalainen liberalismi määrittyikin eurooppalaisia vastineitaan voimakkaammin nuorta valtiota hallinneen kansallisuusajattelun, itsesäilytysvaiston ja kansallisen eheyden vaatimusten kautta. Tutkimuksessa todetaan, että edistyspuolueen eheytyspoliittisen linjan muotoutumista ja toteutumista vuosien 1919‒1939 aikana voi pitää idealismin voittona realismista. Lukuun ottamatta reformipolitiikan vuosia edistyspuolueen pitäytyminen valitulla linjalla näyttäytyi poliittisten toimintamahdollisuuksien kannalta katsottuna ajoittain jopa epärealistiselta. Koko sotien välistä aikaa tarkastellessa voikin todeta, että se, minkä edistyspuolue poliittisten päämäärien saavuttamisen valossa voitti, sen se menetti kannatusluvuissa.

The Pursuit of Efficient Copyright Licensing : How Some Rights Reserved Attempts to Solve the Problems of All Rights Reserved

This dissertation analyses the growing pool of copyrighted works, which are offered to the public using Creative Commons licensing. The study consist of analysis of the novel licensing system, the licensors, and the changes of the "all rights reserved" —paradigm of copyright law. Copyright law reserves all rights to the creator until seventy years have passed since her demise. Many claim that this endangers communal interests. Quite often the creators are willing to release some rights. This, however, is very difficult to do and needs help of specialized lawyers. The study finds that the innovative Creative Commons licensing scheme is well suited for low value - high volume licensing. It helps to reduce transaction costs on several le¬vels. However, CC licensing is not a "silver bullet". Privacy, moral rights, the problems of license interpretation and license compatibility with other open licenses and collecting societies remain unsolved. The study consists of seven chapters. The first chapter introduces the research topic and research questions. The second and third chapters inspect the Creative Commons licensing scheme's technical, economic and legal aspects. The fourth and fifth chapters examine the incentives of the licensors who use open licenses and describe certain open business models. The sixth chapter studies the role of collecting societies and whether two institutions, Creative Commons and collecting societies can coexist. The final chapter summarizes the findings. The dissertation contributes to the existing literature in several ways. There is a wide range of prior research on open source licensing. However, there is an urgent need for an extensive study of the Creative Commons licensing and its actual and potential impact on the creative ecosystem.

Conservation Genetics of Exploited Finnish Salmonid Fishes

Genetic diversity is one of the levels of biodiversity that the World Conservation Union (IUCN) has recognized as being important to preserve. This is because genetic diversity is fundamental to the future evolution and to the adaptive flexibility of a species to respond to the inherently dynamic nature of the natural world. Therefore, the key to maintaining biodiversity and healthy ecosystems is to identify, monitor and maintain locally-adapted populations, along with their unique gene pools, upon which future adaptation depends. Thus, conservation genetics deals with the genetic factors that affect extinction risk and the genetic management regimes required to minimize the risk. The conservation of exploited species, such as salmonid fishes, is particularly challenging due to the conflicts between different interest groups. In this thesis, I conduct a series of conservation genetic studies on primarily Finnish populations of two salmonid fish species (European grayling, Thymallus thymallus, and lake-run brown trout, Salmo trutta) which are popular recreational game fishes in Finland. The general aim of these studies was to apply and develop population genetic approaches to assist conservation and sustainable harvest of these populations. The approaches applied included: i) the characterization of population genetic structure at national and local scales; ii) the identification of management units and the prioritization of populations for conservation based on evolutionary forces shaping indigenous gene pools; iii) the detection of population declines and the testing of the assumptions underlying these tests; and iv) the evaluation of the contribution of natural populations to a mixed stock fishery. Based on microsatellite analyses, clear genetic structuring of exploited Finnish grayling and brown trout populations was detected at both national and local scales. Finnish grayling were clustered into three genetically distinct groups, corresponding to northern, Baltic and south-eastern geographic areas of Finland. The genetic differentiation among and within population groups of grayling ranged from moderate to high levels. Such strong genetic structuring combined with low genetic diversity strongly indicates that genetic drift plays a major role in the evolution of grayling populations. Further analyses of European grayling covering the majority of the species’ distribution range indicated a strong global footprint of population decline. Using a coalescent approach the beginning of population reduction was dated back to 1 000-10 000 years ago (ca. 200-2 000 generations). Forward simulations demonstrated that the bottleneck footprints measured using the M ratio can persist within small populations much longer than previously anticipated in the face of low levels of gene flow. In contrast to the M ratio, two alternative methods for genetic bottleneck detection identified recent bottlenecks in six grayling populations that warrant future monitoring. Consistent with the predominant role of random genetic drift, the effective population size (N_e) estimates of all grayling populations were very low with the majority of N_e estimates below 50. Taken together, highly structured local populations, limited gene flow and the small N_e of grayling populations indicates that grayling populations are vulnerable to overexploitation and, hence, monitoring and careful management using the precautionary principles is required not only in Finland but throughout Europe. Population genetic analyses of lake-run brown trout populations in the Inari basin (northernmost Finland) revealed hierarchical population structure where individual populations were clustered into three population groups largely corresponding to different geographic regions of the basin. Similar to my earlier work with European grayling, the genetic differentiation among and within population groups of lake-run brown trout was relatively high. Such strong differentiation indicated that the power to determine the relative contribution of populations in mixed fisheries should be relatively high. Consistent with these expectations, high accuracy and precision in mixed stock analysis (MSA) simulations were observed. Application of MSA to indigenous fish caught in the Inari basin identified altogether twelve populations that contributed significantly to mixed stock fisheries with the Ivalojoki river system being the major contributor (70%) to the total catch. When the contribution of wild trout populations to the fisheries was evaluated regionally, geographically nearby populations were the main contributors to the local catches. MSA also revealed a clear separation between the lower and upper reaches of Ivalojoki river system – in contrast to lower reaches of the Ivalojoki river that contributed considerably to the catch, populations from the upper reaches of the Ivalojoki river system (>140 km from the river mouth) did not contribute significantly to the fishery. This could be related to the available habitat size but also associated with a resident type life history and increased cost of migration. The studies in my thesis highlight the importance of dense sampling and wide population coverage at the scale being studied and also demonstrate the importance of critical evaluation of the underlying assumptions of the population genetic models and methods used. These results have important implications for conservation and sustainable fisheries management of Finnish populations of European grayling and brown trout in the Inari basin.

"All for one and one for all" Kuinka yhteiskuntavastuu - viestintä on muuttunut suomalaisten pörssiyhtiöiden vuosikertomuksissa vuodesta 2004 vuoteen 2008

Tutkin kandidaatin tutkielmassani yhteiskuntavastuuviestintää suomalaisten pörssiyhtiöiden vuosikertomuksissa 2004. Tutkimus osoitti, että viestintä on hyvin eritasoista eri yrityksissä. Valveutuneet yhteiskuntavastuuviestijät käyttivät kolmen pilarin mallia kategorioidessaan toimintaansa. Selkeästi oli havaittavissa myös toimialakohtaisia eroja. Tässä tutkimuksessa jatkan samalla aihepiirillä selvittämällä sitä, kuinka Helsingin pörssissä listattujen yhtiöiden yhteiskuntavastuuviestintä on muuttunut kun verrataan vuoden 2004 ja 2008 vuosikertomuksia toisiinsa. Tutkimusmetodi on kvalitatiivinen. Diskurssianalyysin keinoin selvitän miten yritykset viestivät vastuullisuudestaan. Tutkimus osoittaa, että yhteiskuntavastuuviestintä ei ole edelleenkään jokaisen yhtiön intresseissä. Yrityksistä noin kaksi kolmesta viestii jotain yhteiskuntavastuun alueeseen liittyvää. Ward on hieman vähentynyt vuodesta 2004. Näistä yrityksistä vastaavasti noin kahdella kolmesta yhteiskuntavastuutoiminta on johdettua ja tavoitteellista tämä näkyy korkealaatuisena yhteiskuntavastuuviestintänä. Taantuma vuosikertomuksissa näkyi etenkin taloudellisen vastuun lisääntyneenä raportointina.

Gavotte (all'antico)

Soitinnus: orkesteri.

Arietta all'antico

Soitinnus: piano.

Menuetto all'antico

Soitinnus: melodia.

It all comes back to you

Soitinnus: big band.