The tightness performance of pre-formed trays as package

Suojakaasupakkaaminen (MAP) on yleistynyt viime aikoina, koska sen avulla voidaan säilöä tuoreita tai vähän käsiteltyjä elintarvikkeita pidempään. Suurin syy hyllyiän pidentymiseen on hiilidioksidin aiheuttama mikrobien kasvun hidastuminen. Toisaalta huolena on patogeenisten mikrobien lisääntyminen anaerobisissa olosuhteissa. Pidempi säilyvyys voidaan saavuttaa myös käyttämällä vähemmän lisä- ja säilöntäaineita. Samalla suojakaasupakkaaminen kuitenkin vähentää myös pilaantuneiden tuotteiden määrää. Eniten suojakaasua käytetään lihan pakkaamisessa. Suojakaasupakkaamisessa elintarvikepakkaukseen syötetään normaalista huoneilmasta poikkeava kaasuseos. Pääasiassa kaasuseos koostuu hiilidioksidista, hapesta ja typestä. Lisäksi voidaan käyttää pieniä määriä hiilimonoksidia, argonia ja rikkidioksidia. Kaasuseoksen koostumus määräytyy elintarvikkeiden ominaisuuksien ja vaatimusten perusteella. Halutun kaasukoostumuksen tulee säilyä pakkauksessa muutamasta päivästä muutamaan kuukauteen riippuen elintarvikkeesta. Siksi tärkein pakkaukselta vaadittava ominaisuus on riittävä kaasutiiveys ja erityisesti hapenläpäisevyys. Koska suurin osa suojakaasupakkauksista on tällä hetkellä muovisia, tutkittiin kokeellisessa osiossa kartonkipakkausten tiiveysominaisuuksia. Kokeet tehtiin vertailemalla erilaisten vuoka- ja kansimateriaalien vaikutusta pakkausten tiiveyteen. Vuokien onnistuminen oli suurin yksittäinen tuloksiin vaikuttanut tekijä. Epäonnistuneen vuoan vaikutukset näkyivät myös saumauksessa, koska saumaustyökalun ja vuoan piti sopia yhteen. Lisäksi näkymättömät mikroreiät hankaloittivat todellisten vuotokohtien paikallistamista. Vuototestausten perusteella materiaaleille löydettiin kuitenkin viitteelliset optimiparametrit. Tärkein saumauksessa vaikuttanut tekijä oli sopivan saumauslämpötilan valinta. Prässättyjen vuokien laatu oli epätasainen. Siksi erityisesti rinnakkaisten kansitus- ja hapenläpäisymittausten väliset erot olivat merkitseviä. Lisäksi prässäys laski materiaalien hapenläpäisyominaisuuksia. Yksittäisten vuokien tiiveysominaisuudet täyttivät kuitenkin kaupallisille kaasupakkauksille asetetut vaatimukset. Vesihöyrynläpäisevyydessä materiaalin vesihöyrynläpäisy oli merkittävämpää kuin vesihöyryn kulkeutuminen vuotokohtien tai epäonnistuneiden saumojen kautta.

Hermetic sealing of food packaging trays

Suojakaasupakkaaminen on lisääntynyt voimakkaasti viime vuosina elintarvikkeiden pakkaamisessa sillä pakkaamalla elintarvike suojakaasuun voidaan sen hyllyikää pidentää ilman säilöntäaineita. Tällainen pakkaaminen vaatii kuitenkin täysin kaasutiiviin pakkauksen, jonka kaasunläpäisevyys on myös alhainen. Yleisimmin käytetyt pakkausmateriaalit suojakaasupakkaamisessa ovat monikerroksiset muovimateriaalit, joissa yhdistyy monen eri muovin parhaimmat ominaisuudet. Yleisimmin käytettyjä muovilaatuja näissä monikerrosrakenteissa ovat PE, PET, PA ja EVOH polymeerit. Myös muita perinteisiä polymeerejä käytetään jonkin verran näissä rakenteissa. Uudemmat muovilaadut, kuten biohajoavat muovit, eivät ole vielä yleistyneet kaupallisessa käytössä pääasiallisesti niiden korkean hinnan vuoksi. Muovisten pakkausten korvaamista esimerkiksi muovipäällystetyillä kartonkipakkauksilla on viime vuosien aikana tutkittu enenevissä määrin. Muovipakkausten korvaamista helpommin kierrätettävillä ja mahdollisesti biohajoavilla materiaaleilla edistävät EU:n direktiivit, jotka käsittelevät pakkausjätteen käsittelyä. Kartonkivuokien saumaamista kaasutiiviisti tutkittiin myös tässä työssä. Tavoitteena oli löytää pakkaus, joka soveltuisi kanasuikaleiden pakkaamiseen suojakaasuun. Kana on herkkä mikrobiologiselle hajoamiselle, minkä johdosta se tulee pakata suojakaasuun jossa happipitoisuuden tulee olla alle 1 % pakkauspäivästä viimeiseen käyttöpäivään saakka. Suorittamalla erilaisia tiiveystutkimuksia voitiin osoittaa, että kartonkivuoka on mahdollista saumata kaasutiiviisti luotettavalla tavalla. Tämä vaatii kuitenkin kartonkivuokien valmistuksen optimoimista päällystemuovikerroksen ja kartongin paksuuden mukaan sekä kannen saumaamista optimoiduilla saumausparametreilla. Tiivein vuoka saavutettiin muovifilmikannella, jonka saumaus perustui samaan muoviin kuin vuoan saumaus. Polyeteenillä saavutettiin tiivein ja kestävin saumaustulos.

Priorization of Customer Needs for Paperboard Trays

The objectives of the study were to introduce current issues of chilled and frozen food packaging, priorize certain customer needs and review brand owners’ opinions and ways of actions. Packaging industry and packaged food markets were reviewed. Interviews of food industry brand owners are used as data sources. Analytic hierarchy process was used to prioritize the customer needs. Food packaging, special features of ready meals, chilled and frozen food packaging, packaging industry and packaged food markets in Europe are approached using literature and market reviews and forecasts. In empirical part the customer needs of paperboard trays are prioritized. The most important features for brand owners are related in product safety and environmental issues. Paperboard trays have benefits compared to its competing packaging solutions. Paperboard is recyclable, from renewable source and it has good printability. Emerging issues of packaging technology are biodegradable package, elderly friendly features such as easiness of opening and re-closing possibility, brand protection and tamper evident solutions.

Effect of ambient conditions on dimensional stability and stiffness of commercial paperboard and paperboard trays

The objective of this study was to develop laboratory test methods for characterizing the effects of changed moisture content on paperboard trays produced by press-forming process. Influence of moisture on the properties of unconverted paperboard such as bending stiffness, bursting strength, and curling was studied. Paperboard and tray samples were tested after storing in different relative humidity conditions (35, 50, 65, 80 and 95% RH). The effect of PE and PET extrusion coatings on these properties was also studied. It was found that increase in moisture content of paperboard decreases bending and bursting strength, dimensional stability and stiffness of paperboard trays. Such physical and mechanical properties as bending stiffness and curling of paperboard seem to define the stiffness of ready-made trays and their dimensional stability. Paperboards and trays with extruded PE and PET one sided coatings demonstrated higher strength properties but at the same time had lower dimensional stability comparing to uncoated paperboards. Samples with smaller polymer coat weight had better dimensional stability than respective samples with higher coat weight. It was also found that preconditioning of paperboard in lower humidity environment before press-forming could improve dimensional stability and stiffness of ready-made tray.

Leak-proof Heat Sealing of Press-Formed Paperboard Trays

Three-dimensional (3D) forming of paperboard and heat sealing of lidding films to trays manufactured by the press forming process are investigated in this thesis. The aim of the work was to investigate and recognize the factors affecting the quality of heat sealing and the leak resistance (tightness) of press-formed, polymer-coated paperboard trays heatsealed with a multi-layer polymer based lidding film. One target was to achieve a solution that can be used in food packaging using modified atmosphere packaging (MAP). The main challenge in acquiring adequate tightness properties for the use of MAP is creases in the sealing area of the paperboard trays which can act as capillary tubes and prevent leak-proof sealing. Several experiments were made to investigate the effect of different factors and process parameters in the forming and sealing processes. Also different methods of analysis, such as microscopic analysis and 3D-profilometry were used to investigate the structure of the creases in the sealing area, and to analyse the surface characteristics of the tray flange of the formed trays to define quality that can be sealed with satisfactory tightness for the use of MAP. The main factors and parameters that had an effect on the result of leak-proof sealing and must be adjusted accordingly were the tray geometry and dimensions, blank holding force in press forming, surface roughness of the sealing area, the geometry and depth of the creases, and the sealing pressure. The results show that the quality of press-formed, polymer-coated paperboard trays and multi-layer polymer lidding films can be satisfactory for the use of modified atmosphere packaging in food solutions. Suitable tools, materials, and process parameters have to be selected and used during the tray manufacturing process and lid sealing process, however. Utilizing these solutions and results makes it possible for a package that is made mostly from renewable and recyclable sources to be a considerable alternative for packages made completely from oil based polymers, and to achieve a greater market share for fibre-based solutions in food packaging using MAP.

Ground beetle (Coleoptera, Carabidae) diversity in Finnish arable land

Appendix: Species of Carabidae and their total catch using pitfall-traps

Development of a Testing Method for Convertibility of Paperboard

Työssä tutkittiin muovattujen kartonkivuokien sekä muovattujen kartonkinäytteiden rinnastettavuutta. Puristusvaiheen prosessiolosuhteiden miellettiin vaikuttavan eniten multidimensionaliseen muodonmuutokseen. Multidimensionaalista muodonmuutosta simuloitiin uudella muovaamiseen soveltuvalla muovauslaitteella. Kirjallisuusosassa keskeisiä teemoja ovat kartongin muovaus sekä kuitupohjaisen materiaalin reologinen käyttäytyminen. Kirjallisuusosassa esitellään lisäksi yksi tekninen sovellus, jonka avulla kyetään ennustamaan kuitumateriaalin muovautuvuutta sekä mittaamaan tapahtunutta muodonmuutosta. Prosessiparametrien teoreettista vaikutustakuituihin tarkastellaan myös kirjallisuusosassa. Kokeellisessa osassa toteutettiin kartonkivuokien valmistus puristamalla. Vastaavilla prosessiparametreilla muovattiin myös pienemmät testinäytteet. Perinteiset yksidimensionaliset deformaatiomittaukset toteutettiin lujuusominaisuuksien laboratoriomäärityksinä. Myös kitka, joka toimii tärkeänä muuttujana prässäysprosessissa, mitattiin laboratorio-olosuhteissa. Tämän työn tulokset osoittavat uuden kehitetyn muovausmenetelmän toimivuuden. Asema-voima kuvaajat ovat selkeitä sekä helposti luettavia. Tuloksissa havaittiin materiaalin muovauspotentiaalin sekä asema-voima kuvaajan välillä vallitseva yhteys. Erittäin merkittävä huomio oli myös, että muovipäällystetyllä kartongilla oli yhteys päällystämättömän kartongin asema-voima kuvaajaan. Tämä tulos osoittaa, että muovipäällystetyn kartongin muovautuvuutta voi olla mahdollista ennustaa pohjakartongin muovautuvuustulosten perusteella. Perinteiset yksidimensionaliset laboratoriomittaukset eivät kykene antamaan riittävää informaatiota muovautuvuuden ennustamiseen. Tästä näkökulmasta on tärkeää että kartongin multidimensionalista muotoutuvuutta voidaankin tutkia kehitetyllä muovausmenetelmällä.

Identifying Critical Business Success Factors of Paperboard Tray

Työn tavoitteena oli kartonkivuoan kriittisten menestystekijöiden ja kilpailuaseman selvittäminen jäähdytettyjen ruokatuotteiden markkinoilla Euroopassa. Kilpailija- ja tavoiteanalyysi suoritettiin kahden suomalaisen pakkaajan kesken. Pakkaajien haastattelut toteutettiin joko henkilökohtaisena tai sähköpostihaastatteluna. Muovi on yleisimmin käytetty jäähdytettyjen ruokatuotteiden pakkausmateriaali. Alumiinivuokien osuus on merkittävä erityisesti laatikkoruokien pakkauksena. Kartonkivuoille on kuitenkin havaittavissa selvää menestyspotentiaalia jäähdytettyjen ruokien pakkauksena. Kartonkivuokien hyvä imago ja edistyksellinen tuotekehitystyö mahdollistavat pakkaajien erityisvaatimuksien täyttämisen ja menestymisen markkinoilla. Kartonkivuoilla on useita ainutlaatuisia kilpailuetu- ja menestystekijöitä, kuten hyvä ulkonäkö ja painojälki. Suurin haaste on saada ruokatuotteiden pakkaajat tietoisiksi kartonkivuokien tuomista pakkausmahdollisuuksista.

Aluminium fouling and its impact on activated carbon based dioxin and furan removal in a wet scrubber at a co-incineration plant

Dioxins and furans, PCDD/Fs, are highly toxic substances formed in post combustion zones in furnaces. PCDD/F emissions are regulated by a waste incineration directive which relates also to co-incineration plants. Several observations of dioxin and furan enhancements in wet scrub- bers have been reported previously. This is thought to be due to the so-called "memory effect" which occurs when dioxins and furans absorb into plastic material in scrubbers and desorb when ambient circumstances alter significantly. At the co-incineration plant involved, dioxins and furans are controlled with a wet scrubber, the tower packing of which is made of plastic in which activated carbon particles are dispersed. This should avoid the memory effect and act as a dioxin and furan sink since dioxins and furans are absorbed irreversibly into the packing ma- terial. In this case, the tower packing in the scrubber is covered with a white layer that has been found to be mainly aluminium. The aim of this thesis was to determine the aluminium balance and the dioxin and furan behaviour in the scrubber and, thus, the impacts that the foul- ing has on dioxin and furan removal. The source of aluminium, reasons for fouling and further actions to minimize its impacts on dioxin and furan removal were also to be discovered. Measurements in various media around the scrubber and in fuels were made and a profile analysis of PCDD/F and mass balance calculations were carried out. PCDD/F content de- creased in the scrubber. The reduced PCDD/F was not discharged into scrubbing water. The removal mechanism seems to work in spite of the fouling, at least with low PCDD/F loads. Most of the PCDD/F in excess water originates from the Kymijoki River which is used as feeding water in the scrubber. Fouling turned out to consist mainly of aluminium hydroxides. Sludge combusted in the furnace was found to be a significant source of aluminium. Ways to minimize the fouling would be adjustment of pH to a proper lever, installation of a mechanical filter to catch the loose material from the scrubbing water and affecting the aluminium content of the sludge.

Vaahdonestokemikaalin syöttötapahtuman tehostamisen vaikutus märkäosan toimintaan

An improved defoamer dosage procedure and a more efficient dosing point to the approach system were studied in this thesis. Their influence on paper machine wet end operations was investigated. The improved defoamer dosing procedure was examined at UMP-Kymmene Tervasaari PM8. Air content and its controlling methods at the paper machine were studied in the literature survey. Also the influence of dissolved gases and entrained air in the papermaking furnish were introduced. Feeding methods – a TrumpJet chemical mixer and traditional feeding devices – were reviewed. The defoamer’s functioning methods were studied. The influence of the use of defoamers was estimated based on the main selected wet end operations. In the experimental part, defoamer mixing with a traditional feeding method and two improved mixing stages were compared based on the air content profiles in PM8’s approach system. The reference dosage procedure was PM8’s old dosing system. The first dosage procedure in the comparison involved two TrumpJet chemical mixers installed on the bottom wire trays. The second element of comparison involved the improvement brought by a third TrumpJet chemical mixer installed on the top wire tray. This second comparison of the efficient defoamer feeding concept was made at a higher production speed of PM8. The air content control situation was also studied at the higher production speed. In addition the connection between the defoamer and air content was observed and a mill-scale system was studied. The economical benefits of the new dosing procedure were also reviewed. Air content profiles of short circulation were measured in the reference situation and the two comparison points of the study. These air content measurements proved the main gas load is introduced to PM8's paper furnish from the white water tray. Thick stock air content was not essential when the air volume flow was considered. The improved defoamer dosing procedure made lower dosage amounts possible. Compared with the traditional feeding system, the new defoamer feeding concept made only few direct improvements to the wet end operations and the produced paper itself. The lower defoamer need was noticed to have a positive influence on hydrophobic sizing and paper defects. The surfaces of the white water tanks and the operation of pumps were assessed based on the density variations of the suspension. The temperature in the white water silo was stated to have a significant influence on the air content measured in the first centrifugal cleaning stage.

Mechanical closing of the paperboard package and the effect of the shape of paperboard package to its manufacturability

The main objective of this thesis was to design a hinge and a closing mechanism for the plastic rim of a paperboard package. Of the hinge and closing mechanisms the 3D-models were designed using SolidWorks program and the functionality of the mechanisms was tested with rapid prototype models. When a mechanism that worked was found, the manufacturability of the mechanisms was tested in an injection molding machine with changeable inserts. Another objective of this thesis was to test the effect of the shape of paperboard package to its manufacturability. The effect of the packages shape was tested with plastic tools made for three different shaped trays. Suggestions for further research were made according to the results of the thesis.

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.

Kartonkimateriaalien muotoutuvuus vuokien valmistuksessa

Diplomityön tavoitteena oli tutkia erilaisten elintarvikekartonkien muotoutuvuutta prässäämällä valmistettujen vuokien valmistuksessa. Kirjallisuusosassa käsiteltiin mm. kartongin muotoutuvuuteen vaikuttavia ominaisuuksia sekä lämpötilan ja kosteuden vaikutusta muotoutuvuuteen. Lisäksi kirjallisuusosassa käytiin läpi vuokien valmistusprosessi, jossa vuoka-aihiot valmistetaan stanssaamalla ja vuoat prässäämällä. Lopuksi on esitetty vuokien valmistuksessa kartongin muotoutuvuuteen vaikuttavia ajoparametrejä. Kokeellisessa osassa valmistettiin prässäämällä vuokia erilaisista kartonkimateriaaleista. Jokaiselle materiaalille etsittiin sopivat ajoparametrit erilaisissa kosteuspitoisuuksissa ja vertailtiin niiden muotoutuvuutta. Työ sisälsi myös kaksi laminointikoeajoa, jonka tuloksena saatuja materiaaleja verrattiin referenssi vuokakartonkiin. Vuokien todettiin muotoutuvan parhaiten kosteuden ollessa 7 – 9,4 % välillä. Työssä erottui kartongit, jotka muotoutuivat muita paremmin sekä kartongit, jotka muotoutuivat muita huonommin. Näiden muotoutuvuutta pyrittiin selvittämään mitattujen paperiteknisten ominaisuuksien avulla, mutta selvää yksittäistä selittävää ominaisuutta ei löytynyt. Parhaiten muotoutuvuutta kuvasivat kartonkien kuitukoostumukset. Laminoitujen rakenteiden todettiin muotoutuvan vuokakartonkia paremmin. Tähän vaikuttivat laminaattien korkeammat lujuus- ja venymäarvot.

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.

Kielikylpydidaktiikkaa kehittämässä : 3-6-vuotiaiden kielikylpylasten kielellinen kehitys ja kielikylpydidaktiikan kehittäminen päiväkodissa

The goal of this study is to determine the naming ability in Finnish and Swedish of nursery school-aged children participating in a language immersion programme, as well as their command of both languages. The study also aims to describe factors reflecting language immersion teaching in nursery schools based on action research and a literature survey. The longitudinal study, conducted in 2003–2005, comprised 133 native Finnish three- to six-year-old children in language immersion programmes. A total of four measurements were carried out over two and a half years. In each measurement, four separate tests were given to each child (totally 1134 measurements). Research material was collected using survey tools that measured the children’s naming ability and command of language. The tools had been translated into both Finnish and Swedish. The material also includes taped responses related to the tool for naming ability. Didactic approaches were developed on the basis of material from action research and the literature survey. The material was examined using methodological triangulation, and a quantitative analysis was made of each survey tool. Furthermore, a content analysis of the children’s taped responses gave further depth to the description of language development. The theoretical framework of the study is mainly based on modern sociocultural theories of second language development and acquisition. Thus, the approach is both linguistic and pedagogic, with emphasis lying on the latter. The socioculturally-oriented framework of this study is mainly influenced by the theorists Vygotski, Spolsky, van Lier and Cummins. According to the results, the language skills of children in language immersion programmes develop as expected from age three to six in the fields studied. In the field of language command, the children acquired excellent skills in listening comprehension. Their naming ability was not as good. In each test, the children showed weaker skills in Swedish than in Finnish. However, based on the assumption that the two languages have a shared cognitive field, the skills in Swedish catch up with the skills in Finnish at an annual rate of 6–7 per cent. The study indicates that children meet a language development threshold one year earlier in their native language than they do in the immersion language. As for the naming ability in Swedish, problems arose from the fact that the deviation in results increases with age. Children showed creativity in their use of naming strategies. Judging by the research results, children begin to use the immersion language as a tool for thought at a very early phase. The research results, action research and literature survey were also used to create a general educational model for language immersion.