Enhancing performance of paper coatings by tailor-made plastic pigments

The paper industry is constantly looking for new ideas for improving paper products while competition and raw material prices are increasing. Many paper products are pigment coated. Coating layer is the top layer of paper, thus by modifying coating pigment also the paper itself can be altered and value added to the final product. In this thesis, synthesis of new plastic and hybrid pigments and their performance in paper and paperboard coating is reported. Two types of plastic pigments were studied: core-shell latexes and solid beads of maleimide copolymers. Core-shell latexes with partially crosslinked hydrophilic polymer core of poly(n-butyl acrylate-co-methacrylic acid) and a hard hydrophobic polystyrene shell were prepared to improve the optical properties of coated paper. In addition, the effect of different crosslinkers was analyzed and the best overall performance was achieved by the use of ethylene glycol dimethacrylate (EGDMA). Furthermore, the possibility to modify core-shell latex was investigated by introducing a new polymerizable optical brightening agent, 1-[(4-vinylphenoxy)methyl]-4-(2-henylethylenyl)benzene which gave promising results. The prepared core-shell latex pigments performed smoothly also in pilot coating and printing trials. The results demonstrated that by optimizing polymer composition, the optical and surface properties of coated paper can be significantly enhanced. The optimal reaction conditions were established for thermal imidization of poly(styrene-co-maleimide) (SMI) and poly(octadecene-co-maleimide) (OMI) from respective maleic anhydride copolymer precursors and ammonia in a solvent free process. The obtained aqueous dispersions of nanoparticle copolymers exhibited glass transition temperatures (Tg) between 140-170ºC and particle sizes from 50-230 nm. Furthermore, the maleimide copolymers were evaluated in paperboard coating as additional pigments. The maleimide copolymer nanoparticles were partly imbedded into the porous coating structure and therefore the full potential of optical property enhancement for paperboard was not achieved by this method. The possibility to modify maleimide copolymers was also studied. Modifications were carried out via N-substitution by replacing part of the ammonia in the imidization reaction with amines, such as triacetonediamine (TAD), aspartic acid (ASP) and fluorinated amines (2,2,2- trifluoroethylamine, TFEA and 2,2,3,3,4,4,4-heptafluorobuthylamine, HFBA). The obtained functional nanoparticles varied in size between 50-217 nm and their Tg from 150-180ºC. During the coating process the produced plastic pigments exhibited good runnability. No significant improvements were achieved in light stability with TAD modified copolymers whereas nanoparticles modified with aspartic acid and those containing fluorinated groups showed the desired changes in surface properties of the coated paperboard. Finally, reports on preliminary studies with organic-inorganic hybrids are presented. The hybrids prepared by an in situ polymerization reaction consisted of 30 wt% poly(styrene- co-maleimide) (SMI) and high levels of 70 wt% inorganic components of kaolin and/or alumina trihydrate. Scanning Electron Microscopy (SEM) images and characterization by Fourier Transform Infrared Spcetroscopy (FTIR) and X-Ray Diffraction (XRD) revealed that the hybrids had conventional composite structure and inorganic components were covered with precipitated SMI nanoparticles attached to the surface via hydrogen bonding. In paper coating, the hybrids had a beneficial effect on increasing gloss levels.

Chaotic Behaviour of Active Magnetic Bearing System by Time Series Analysis

Chaotic behaviour is one of the hardest problems that can happen in nonlinear dynamical systems with severe nonlinearities. It makes the system's responses unpredictable. It makes the system's responses to behave similar to noise. In some applications it should be avoided. One of the approaches to detect the chaotic behaviour is nding the Lyapunov exponent through examining the dynamical equation of the system. It needs a model of the system. The goal of this study is the diagnosis of chaotic behaviour by just exploring the data (signal) without using any dynamical model of the system. In this work two methods are tested on the time series data collected from AMB (Active Magnetic Bearing) system sensors. The rst method is used to nd the largest Lyapunov exponent by Rosenstein method. The second method is a 0-1 test for identifying chaotic behaviour. These two methods are used to detect if the data is chaotic. By using Rosenstein method it is needed to nd the minimum embedding dimension. To nd the minimum embedding dimension Cao method is used. Cao method does not give just the minimum embedding dimension, it also gives the order of the nonlinear dynamical equation of the system and also it shows how the system's signals are corrupted with noise. At the end of this research a test called runs test is introduced to show that the data is not excessively noisy.

Topochemistry of physical and chemical pretreatments of biomass as investigated by FE-SEM, XPS and ToF-SIMS

Surface chemistry is of great importance in plant biomass engineering and applications. The surface chemical composition of biomass which includes lignin, carbohydrates and extractives influences its interactions with chemical agents, such as pulp processing/papermaking chemicals, or enzymes for different purposes. In this thesis, the changes in the surface chemical composition of lignocellulosic biomass after physical modification for the improvement of resulting paper properties and chemical treatment for the enhancement of enzymatic hydrolysis were investigated. Low consistency (LC) refining was used as physical treatment of bleached softwood and hardwood pulp samples, and the surface chemistry of refined samples was investigated. The refined pulp was analysed as whole pulp while the fines-free fibre samples were characterized separately. The fines produced in LCrefining contributed to an enlarged surface specific area as well as the change of surface coverage by lignin and extractives, as investigated by X-ray photoelectron spectroscopy (XPS). The surface coverage by lignin of the whole pulp decreased after refining while the surface coverage by extractives increased both for pine and eucalyptus. In the case of pine, the removal of fines resulted in reduction of the surface coverage by extractives, while the surface coverage by lignin increased on fibre sample (without fines). In the case of eucalyptus, the surface coverage by lignin of fibre samples decreased after the removal of fines. In addition, the surface distribution of carbohydrates, lignin and extractives of pine and eucalyptus samples was determined by Time-of-Flight Secondary Ion Mass Spectrometry (ToF-SIMS). LC-refining increased the amounts of pentose, hexose and extractives on the surface of pine samples. ToF-SIMS also gave clear evidence about xylan deposition and reduction of surface lignin distribution on the fibre of eucalyptus. However, the changes in the surface chemical composition during the physical treatment has led to an increase in the adsorption of fluorescent whitening agents (FWAs) on fibres due to a combination of electro-static forces, specific surface area of fibres and hydrophobic interactions. Various physicochemical pretreatments were conducted on wood and non-wood biomass for enhancing enzymatic hydrolysis of polysaccharides, and the surface chemistry of the pretreated and enzymatically hydrolysed samples was investigated by field emission scanning electron microscopy (FE-SEM), XPS and ToF-SIMS. A hydrotrope was used as a relatively novel pretreatment technology both in the case of wood and non-wood biomass. For comparison, ionic liquid and hydrothermal pretreatments were applied on softwood and hardwood as well. Thus, XPS analysis showed that the surface lignin was more efficiently removed by hydrotropic pretreatment compared to ionic liquid or hydrothermal pretreatments. SEM analysis also found that already at room temperature the ionic liquid pretreatments were more effective in swelling the fibres compared with hydrotropic pretreatment at elevated temperatures. The enzymatic hydrolysis yield of hardwood was enhanced due to the decrease in surface coverage of lignin, which was induced by hydrotropic treatment. However, hydrotropic pretreatment was not appropriate for softwood because of the predominance of guaiacyl lignin structure in this material. In addition, the reduction of surface lignin and xylan during pretreatment and subsequent increase in cellulose hydrolysis by enzyme could be observed from ToF-SIMS results. The characterisation of the non-wood biomass (e.g. sugarcane bagasse and common reed) treated by hydrotropic method, alkaline and alkaline hydrogen peroxide pretreatments were carried out by XPS and ToF-SIMS. According to the results, the action for the removal of the surface lignin of non-wood biomass by hydrotropic pretreatment was more significant compared to alkaline and alkaline hydrogen peroxide pretreatments, although a higher total amount of lignin could be removed by alkaline and alkaline hydrogen peroxide pretreatment. Furthermore, xylan could be remarkably more efficiently removed by hydrotropic method. Therefore, the glucan yield achieved from hydrotropic treated sample was higher than that from samples treated with alkaline or alkaline hydrogen peroxide. Through the use of ToF-SIMS, the distribution and localization of lignin and carbohydrates on the surface of ignocelluloses during pretreatment and enzymatic hydrolysis could be detected, and xylan degradation during enzymatic hydrolysis could also be assessed. Thus, based on the results from XPS and ToF-SIMS, the mechanism of the hydrotropic pretreatment in improving the accessibility of enzymes to fibre and further ameliorating of the enzymatic saccharification could be better elucidated.

Enhancing the Usability of Drug Materials by Electrostatic Atomisation

Electrospraying or electrostatic atomisation is a process of liquid disruption by electrostatic forces. When liquid is brought into an electric field, charge is induced to its surface. Once the repulsive electrostatic force exceeds the liquid surface tension, the liquid disrupts into small highly charged droplets. The size of the electrosprayed droplets can range from hundreds of micrometers down to a few tens of nanometers. Electrospraying can be used not only to produce droplets, but also solid particles. The research presented in this thesis concentrates on producing drug particles by this method. In the experiments, a drug powder was dissolved in a convenient solvent and the solution was atomised. The solvent was then evaporated from the formed droplets in a drying medium and inside each droplet, a dense cluster of the dissolved drug remained. From the pharmaceutical point of view, the most important characteristics of the produced particles are size distribution, porosity, crystal form and degree of crystallinity. These properties affect the dissolution behaviour and ultimately the drug bioavailability in the body. The effects of electrostatic atomization on the aforementioned characteristics are generally not well understood. The research focused on studying these particle properties and finding possible correlations with the spraying parameters. The produced droplets were dried either under atmospheric or reduced pressure, the latter in order to improve the drying process. Special emphasis was put on implementing the spraying under reduced pressure, and the effects of the drying pressure on particle properties. Based on the results, the possibilities to enhance the dissolution of poorly soluble drugs by this method were estimated. In the course of experiments, it was also discovered that electrospraying may have a profound effect on the polymorphic form of the produced drug particles. In the light of the obtained results, it was concluded that electrospraying may offer a valuable tool to overcome some of the challenges met in modern drug development and formulation.

Sähköverkkotiedonsiirtomenetelmän kehittäminen taajuusmuuttajaohjattuihin sähkökäyttöihin

Sähkömoottorin jatkuva-aikainen kunnonvalvonta vaatii tiedonsiirtoa moottorilta ylemmälle tietojärjestelmätasolle, kuten taajuusmuuttajalle. Uusien kaapeleiden asennus on työlästä ja kallista. Moottorin ja taajuusmuuttajan välillä on kuitenkin aina kaapeli, jota käytetään moottorin tehonsyöttöön. Tätä kaapelia on mahdollista käyttää myös tiedonsiirtokanavana. Tässä diplomityössä käsitellään ja tutkitaan sähköverkkotiedonsiirtomenetelmää, jonka avulla voidaan muodostaa Ethernet-yhteys moottorilta taajuusmuuttajalle tai toisinpäin. Työssä kehitetään simulointimalli tiedonsiirtokanavan taajuusriippuvan vaimennuksen simuloimiseen. Lisäksi kehitetään kytkentärajapinta, joka mahdollistaa tiedonsiirron kolmivaiheisessa taajuusmuuttajan syöttämässä moottorikaapelissa. Työssä suunnitellaan ja toteutetaan tiedonsiirtoa varten pilot-laitteisto, jolla tehdään laboratoriotestit. Laboratoriotesteillä varmistetaan menetelmän soveltuvuus. Laboratoriotestien avulla etsitään myös reunaehdot tiedonsiirron toiminnalle ja tiedonsiirtonopeuteen vaikuttavia tekijöitä taajuusmuuttajakäytössä. Lisäksi tarkastellaan menetelmän aiheuttamaa viivettä, joka on tärkeäsäätösovellusten kannalta. Lopuksi arvioidaan menetelmän soveltuvuus käytännön sovelluksiin.

Jätteenpolton tuhkien käsittelytekniikoiden ympäristövaikutukset

Jätteenpoltossa syntyvät tuhkat sisältävät paljon haitta-aineita, joiden vuoksi niitä ei yleensä voida suoraan sijoittaa kaatopaikoille. Käsittelyllä pyritään parantamaan tuhkien ominaisuuksia ja vähentämään haitta-aineiden liukoisuutta. Samalla kuitenkin käsittely kuluttaa raaka-aineita ja energiaa sekä aiheuttaa päästöjä. Tuhkien käsittelyn kokonaishyötyjä ja -haittoja ympäristön kannalta arvioitaessa tulisikin ottaa huomioon sekä käsiteltävän tuhkan parantuneet ominaisuudet että käsittelystä aiheutuneet ympäristökuormitukset. Tämän diplomityön tavoitteena oliselvittää jätteenpolton tuhkien käsittelystä aiheutuvia ympäristövaikutuksia tarkastelemalla esimerkinomaisesti neljää erilaista käsittelytekniikkaa (pesua, sementtikiinteytystä, Ferrox-prosessia ja vitrifiointia) sekä kahta muuta loppusijoitusvaihtoehtoa (mahdollisuutta sijoittaa tuhkat kaatopaikalle ilman käsittelyä ja kuljettamista Norjassa sijaitsevalle käsittely- ja loppusijoituslaitokselle). Tarkastelussa keskityttiin jätteenpolton ongelmallisimpiin tuhkajakeisiin, lentotuhkaan ja savukaasujen puhdistusjätteisiin eli APC-jätteisiin. Tavoitteena oli selvittää käsittelyvaihtoehdoista syntyvät ympäristökuormitukset ns. koko niiden elinkaaren ajalta, eli huomioiden käsittelyyn tarvittavien lisäaineiden valmistuksesta, itse käsittelyprosessista sekä loppusijoituksesta aiheutuvat kuormitukset. Tarkastelun perusteella eri käsittelyvaihtoehdot aiheuttavat hyvin erilaisia ja erisuuruisia ympäristökuormituksia. Lisäksi käsitellyn materiaalin ominaisuudet vaihtelevat huomattavasti käsittelytavasta riippuen. Tarkastelluista käsittelyvaihtoehdoista suurimmat ympäristökuormitukset ilmapäästöjen osalta aiheutuivat tyypillisesti joko käsittelyyn tarvittavien raaka-aineiden valmistuksesta tai itse käsittelyprosessin energiankulutuksesta. Loppusijoituksesta sen sijaan aiheutui ympäristöhaittoja kaatopaikkarakenteiden muodostamisesta sekä maaperään vapautuvista haitta-aineista, joiden määrä riippuu tuhkan käsittelyn tehokkuudesta.

Ylisoonisen yksivaiheisen aksiaaliturbiinin suunnittelu

Tässä diplomityössä suunnitellaan yksivaiheisen turbiinin ylisooninen staattori ja alisooninen roottori, tulo-osa ja diffuusori. Työn alussa tarkastellaan aksiaaliturbiinin käyttökohteita ja teoriaa, jonka jälkeen esitetään suunnittelun perustana olevat menetelmät ja periaatteet. Perussuunnittelu tehdään Traupelinmenetelmällä WinAxtu 1.1 suunnitteluohjelmalla ja hyötysuhde arvioidaan lisäksiExcel-pohjaisella laskennalla. Ylisooninen staattori suunnitellaan perussuunnittelun tuloksiin perustuen, soveltamalla karakteristikoiden menetelmää suuttimen laajenevaan osaan ja pinta-alasuhteita suppenevaan osaan. Roottorin keskiviiva piirretään Sahlbergin menetelmällä ja siiven muoto määritetään A3K7 paksuusjakauman sekä tiheän siipihilan muotoilun periaatteita yhdistämällä. Tulo-osa suunnitellaan mahdollisimman jouhevaksi geometriatietojen ja kirjallisuuden esimerkkien mukaisesti. Lopuksi tulo-osaa mallinnetaan CFD-laskennalla. Diffuusori suunnitellaan käyttämällä soveltuvin osin kirjallisuudessa esitettyjätietoja, tulo-osan geometriaa ja CFD-laskentaa. Suunnittelutuloksia verrataan lopuksi kirjallisuudessa esitettyihin tuloksiin ja arvioidaan suunnittelun onnistumista sekä mahdollisia ongelmakohtia.

Galvanomagnetic effects in strongly doped p-Bi2Te3:Sn crystals

Magnetic field dependencies of Hall coefficient and magnetoresistivity are investigated in classical and quantizing magnetic fields in p-Bi2Te3 crystals heavily doped with Sn grown by Czochralsky method. Magnetic field was parallel to the trigonal axis C3. Shubnikov-de Haas effect and quantum oscillations of the Hall coefficient were measured at temperatures 4.2 K and 11 K. On the basis of the magnetic field dependence of the Hall coefficient a method of estimation of the Hall factor and Hall mobility using the Drabble- Wolf six ellipsoid model is proposed. Shubnikov-de Haas effect and quantum oscillations of the Hall coefficient were observed at 4.2 K and 11 K. New evidence for the existence of the narrow band of Sn impurity states was shown. This band is partly filled by electrons and it is overlapping with the valence states of the light holes. Parameters of the impurity states, their energy ESn - 15 meV, band broadening ¿<< k0T and localization radius of the impuritystate R - 30 Å were obtained.

Nopeasti liukenevien lääkeaineiden liukenemisnopeuden mittaaminen optisesti

Työssä perehdytään nopeasti liukenevien lääkeaineiden liukenemisnopeuden mittaamiseen optisesti. Tavoitteena olikehittää mittausjärjestely, jolla liukenemisen optinen mittaaminen olisi mahdollista. Työn kirjallisessa osiossa perehdytään liukenemisen teoriaan sekä mittauksien kannalta tärkeään valon absorption ja sironnan teoriaan. Työn kokeellisessa osassa tarkastellaan liukenemisnopeuden mittaamista,sitä varten kehitetyllä mittausjärjestelyllä sekä pohditaan menetelmänsoveltuvuutta nopeasti liukenevien lääkeaineiden liukenemisnopeuden mittaamiseen. Liukenemisnopeuden optinen mittaaminen osoittautui vaikeaksi joissakin tapauksissa pienten hiukkasten keveyden johdosta. Kevyet hiukkaset kostuivat liian hitaasti, mikä aiheutti ongelmia mittauksiin. Nopeasti kostuvilla hiukkasilla liukenemisnopeuden määrittäminen mittaus-signaalin perusteella oli huomattavasti helpompaa. Näillä aineilla mittaukset onnistuivat hyvin.

More than Words? An Analysis on the Language and Structure of General Election Manifestos of the British Labour Party 1983-2005

The topic of this study is the language of the educational policies of the British Labour party in the General Election manifestos between the years 1983-2005. The twenty-year period studied has been a period of significant changes in world politics, and in British politics, especially for the Labour party. The emergence educational policy as a vote-winner of the manifestos of the nineties has been noteworthy. The aim of the thesis is two-fold: to look at the structure of the political manifesto as an example of genre writing and to analyze the content utilizing the approach of critical discourse analysis. Furthermore, the aim of this study is not to pinpoint policy positions but to look at what is the image that the Labour Party creates of itself through these manifestos. The analysis of the content is done by a method of close-reading. Based on the findings, the methodology for the analysis of the content was created. This study utilized methodological triangulation which means that the material is analyzed from several methodological aspects. The aspects used in this study are ones of lexical features (collocation, coordination, euphemisms, metaphors and naming), grammatical features (thematic roles, tense, aspect, voice and modal auxiliaries) and rhetoric (Burke, Toulmin and Perelman). From the analysis of the content a generic description is built. By looking at the lexical, grammatical and rhetorical features a clear change in language of the Labour Party can be detected. This change is foreshadowed already in the 1992 manifesto but culminates in the 1997 manifesto which would lead Labour to a landslide victory in the General Election. During this twenty-year period Labour has moved away from the old commitments and into the new sphere of “something for everybody”. The pervasiveness of promotional language and market inspired vocabulary into the sphere of manifesto writing is clear. The use of the metaphors seemed to be the tool for the creation of the image of the party represented through the manifestos. A limited generic description can be constructed from the findings based on the content and structure of the manifestos: especially more generic findings such as the use of the exclusive we, the lack of certain anatomical parts of argument structure, the use of the future tense and the present progressive aspect can shed light to the description of the genre of manifesto writing. While this study is only the beginning, it proves that the combination of looking at the lexical, grammatical and rhetorical features in the study of manifestos is a promising one.

The high-speed induction motor: calculating the effects of solid-rotor material on machine characteristics

A method for the analysis of high-speed solid-rotor induction motors in presented. The analysis is based on a new combination of the three dimensional linear method and the transfer matrix method. Both saturation and finite length effects are taken into account. The active region of the solid rotor is divided into saturated and unsaturated parts. The time dependence is assumed to be sinusoidal and phasor quantities are used in the solution. The method is applied to the calculation of smooth solid rotors manufactured of different materials. Six rotor materials are tested: three construction steels, pure iron, a cobaltiron alloy and an aluminium alloy. The results obtained by the method agree fairly well with the measurement quantities.

Kansainvälisen liiketoimintaosaamisen kehittämistarpeet suomalaisissa pk-yrityksissä

Tämän pro gradu -tutkielman tavoitteena oli kartoittaa suomalaisten pk-yritysten kansainvälisen liiketoimintaosaamisen kehittämistarpeita ja esittää kuinka kansainvälistymispalveluita voitaisiin kehittää vastaamaan tarpeisiin paremmin. Tutkielma jakautuu teoreettiseen ja empiiriseen osaan. Empiirisessä osassa hyödynnettiin valmista, survey-menetelmällä toteutettua tutkimusmateriaalia, jonka 122 pk-yritystä tutkittiin kvantitatiivisesti. Tutkimuksen mukaan suomalaisten pk-yritysten keskeisin kansainvälisen liiketoimintaosaamisen kehittämistarve on myynti- ja markkinointi-osaaminen. Pk-yritykset tarvitsevat ulkopuolista apua erityisesti ulkomaisten asiakkaiden ja yhteistyökumppaneiden löytämisessä. Tutkimuksen mukaan kansainvälistymispalveluiden käyttämättä jättämiseen ei vaikuta se, ettei palveluista ole saatu tarpeeksi tietoa, vaan se, ettei palveluita koeta hyödyllisiksi ja tarpeisiin vastaaviksi. Pk-yritysten kansainvälisen osaamisen kehittämiseen tarjottavat palvelut eivät täysin vastaa yritysten tarpeita. Kansainvälistymispalveluita tulisi kehittää erityisesti tarjoamalla yrityksille käytännön apua koulutuksen sijasta, tunnistamalla osaamistarpeet tehokkaammin, parantamalla alueellista tiedotusta ja lisäämällä palveluntarjoajien keskeistä yhteistyötä.

NMR in Crystals and Powders of Topazes with Different Colours

The present work is a part of the large project with purpose to investigate microstructure and electronic structure of natural topazes using NMR method. To reach this task we determined the relative contents of fluorine and hydrogen in crystals blue, colorless, wine and wine irradiated topazes. Then we determined the electric field gradients in site of aluminium atoms by NMR method, calculated EFG using ab initio method, and measured relaxation time dependence on heating temperature for blue, colorless, Swiss blue and sky blue topazes. Nuclear magnetic resonance (NMR) is an effective method to investigate the local structure in the crystal. The NMR study of the single crystal gives detailed information especially about the local crystal structure. As a result of this work we have received practical data, which is possible to use in future for making personal dosimetry and for preparation of mullite, which is widely used in traditional and advanced ceramic materials.

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.

Toimittajan oikeus uutisoida ja toimitustyötä sääntelevät normit

Luettaessa uutisia lehdestä harvoin pohditaan sitä, onko toimituksellisessa työssä noudatettu lakia ja alan eettisiä ohjeita. Lukija luottaa siihen, että sääntöjä noudatetaan, mutta näin ei aina ole. Käytettäessä materiaalia toiselta lehdeltä jätetään alkuperäinen lähde usein mainitsematta. Tämän tutkielman tarkoituksena on selvittää keskeiset tekijänoikeuslain pykälät ja käytännössä kaikkein keskeisimmät Journalistin ohjeet sanomalehden toimittajan työssä ja miten nämä säännöt pääosin ilmenevät. Suoritetun kyselytutkimuksen perusteella tekijänoikeuslain pykälä oikeus uutisoida toisen lehden uutinen ja Journalistin ohjeista sääntö, jonka mukaan sisältöratkaisut on tehtävä journalistisin perustein, ovat keskeisimpiä sääntöjä käytännön työssä. Tutkimuksessa näitä sääntöjä käsitellään oikeusdogmaattisin menetelmin kieliopillisen tulkinnan kautta sekä toimittajan työn näkökulmasta. Tutkimuksen lainsäädännöllisen viitekehyksen muodostavat Suomen perustuslaki, laki sananvapauden käyttämisestä joukkoviestinnässä, kansallinen tekijänoikeuslaki ja Journalistin ohjeet. Tämän vuoksi tutkimuksessa on aiheellista tarkastella myös sananvapautta ja tekijänoikeuslakia toimituksellisessa työssä sekä näiden suhdetta toisiinsa ja myös median rakenteellista ja toiminnallista muutosta.