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.

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.

Enabling constructive alignment in programming instruction

In this thesis, simple methods have been sought to lower the teacher’s threshold to start to apply constructive alignment in instruction. From the phases of the instructional process, aspects that can be improved with little effort by the teacher have been identified. Teachers have been interviewed in order to find out what students actually learn in computer science courses. A quantitative analysis of the structured interviews showed that in addition to subject specific skills and knowledge, students learn many other skills that should be mentioned in the learning outcomes of the course. The students’ background, such as their prior knowledge, learning style and culture, affects how they learn in a course. A survey was conducted to map the learning styles of computer science students and to see if their cultural background affected their learning style. A statistical analysis of the data indicated that computer science students are different learners than engineering students in general and that there is a connection between the student’s culture and learning style. In this thesis, a simple self-assessment scale that is based on Bloom’s revised taxonomy has been developed. A statistical analysis of the test results indicates that in general the scale is quite reliable, but single students still slightly overestimate or under-estimate their knowledge levels. For students, being able to follow their own progress is motivating, and for a teacher, self-assessment results give information about how the class is proceeding and what the level of the students’ knowledge is.

Sulfuric acid - glucose separation using mixed-recycle steady state recycling chromatography

Batch chromatography is a widely used separation technique in a variety of fields meeting difficult separations. Several technologies for improving the performance of chromatography have been studied, including mixed-recycle steady state recycling (MR-SSR) chromatography. Design of MR-SSR has been commonly limited on 100 % purity constraint cases and empirical work. In this study a predictive design method was used to optimize feed pulse size and design a number of experimental MR-SSR separations for a solution of 20 % sulfuric acid and 100 g/L glucose. The design was under target product fraction purities of 98.7 % for H2SO4 and 95 % for glucose. The experiments indicate a maximum of 59 % increase in sulfuric acid productivity and 82 % increase for glucose when compared to corresponding batch separation. Eluent consumption was lowered by approximately 50 % using recycling chromatography. Within this study the target purities and yields set in design were not completely met, and further optimization of the process is deemed necessary.

Memristive Computing

Memristive computing refers to the utilization of the memristor, the fourth fundamental passive circuit element, in computational tasks. The existence of the memristor was theoretically predicted in 1971 by Leon O. Chua, but experimentally validated only in 2008 by HP Labs. A memristor is essentially a nonvolatile nanoscale programmable resistor — indeed, memory resistor — whose resistance, or memristance to be precise, is changed by applying a voltage across, or current through, the device. Memristive computing is a new area of research, and many of its fundamental questions still remain open. For example, it is yet unclear which applications would benefit the most from the inherent nonlinear dynamics of memristors. In any case, these dynamics should be exploited to allow memristors to perform computation in a natural way instead of attempting to emulate existing technologies such as CMOS logic. Examples of such methods of computation presented in this thesis are memristive stateful logic operations, memristive multiplication based on the translinear principle, and the exploitation of nonlinear dynamics to construct chaotic memristive circuits. This thesis considers memristive computing at various levels of abstraction. The first part of the thesis analyses the physical properties and the current-voltage behaviour of a single device. The middle part presents memristor programming methods, and describes microcircuits for logic and analog operations. The final chapters discuss memristive computing in largescale applications. In particular, cellular neural networks, and associative memory architectures are proposed as applications that significantly benefit from memristive implementation. The work presents several new results on memristor modeling and programming, memristive logic, analog arithmetic operations on memristors, and applications of memristors. The main conclusion of this thesis is that memristive computing will be advantageous in large-scale, highly parallel mixed-mode processing architectures. This can be justified by the following two arguments. First, since processing can be performed directly within memristive memory architectures, the required circuitry, processing time, and possibly also power consumption can be reduced compared to a conventional CMOS implementation. Second, intrachip communication can be naturally implemented by a memristive crossbar structure.

Specific surface charging of latex, clay and mineral oxide particles in aqueous, non-aqueous and mixed solvent systems

En djupare förståelse för växelverkan mellan partiklar i suspensioner är av betydelse för utvecklingen av en mängd olika industriella produkter och processer. Till exempel kan nämnas pigmentbaserade färger och bestrykning av papper. Genom att öka kontrollbarheten kan dessa lättare optimeras för att uppnå förbättrade produktegenskaper och/eller sänkta produktionskostnader. Av stor betydelse är även en förbättrad möjlighet att minska produktens miljöpåverkan. I avhandlingen studerades jonstyrkan och jonspecificiteten inverkan i olika akvatiska suspensioner innehållande olika elektrolyter. De partiklar som avhandlingen omfattade var metalloxider, leror samt latex. Jonstyrkan studerades från låga (c <10-3M) till och med höga (c> 10-1M) elektrolytkoncentrationer. Vid koncentrationer under 0.1 M var partikelladdningen styrd av pH och jonstyrkan. Vid högre elektrolytkoncentrationer påverkade även jonspecificiteten partikelladdningen. Jonspecificiteten arrangerades i fenomenologiska serier funna i litteraturen samt med Born modellen definierad i termodynamiken. Överraskande höga absoluta zeta-potential värden erhölls vid höga elektrolytkoncentrationer vilket visar att den elektrostatiska repulsionen har betydelse även vid dessa förhållanden. Vidare studerades titanoxidsuspensioners egenskaper i akvatiska, icke-akvatiska och blandade lösningssystem under varierande koncentration av oxal- och fosfatsyra. Vid lågt vatteninnehåll studerades även suspensioner med svavelsyra. Konduktiviteten i suspensioner med lågt vatteninnehåll ökade med tillsatt oxal- eller fosforsyra vilket är en omvänd effekt jämfört med svavelsyra eller akvatiska suspensioner. Den omvända effekten skiftade gradvis tillbaka med ökad vatteninnehåll. En analys av suspensionernas adsorption i höga etanolkoncentrationer gjordes med konduktiviteten, pH och zeta-potentialen. Viskositet studerades och applicerades framgångsrikt i viskositet/ytladdningsmodeller utvecklade för akvatiska suspensioner.

Applying Qt to programming courses

Työn tavoitteena on sovittaa Qt opetussuunnitelmaan. Työ sisältää Qt:n lyhyen historian sekä katsauksen sen nykytilaan. Nykytilakatsaus sisältää kolme näkökulmaa: miten ja missä Qt:ta voidaan käyttää, sekä sen käyttötarkoitukset teollisuudessa ja opetuksessa. Työn tuloksena syntyy luentodemonstraatiota varten pieni ohjelma, joka on luotu C++:n ja Qt Designerin avulla ja käyttää olennaisia käyttöliittymäkirjaston olioita. Toisena tuotteena työssä syntyy luonnos Lappeenrannan Teknillisen Yliopiston ohjelmointikursseista, joissa Qt:ta voitaisiin käyttää avustamaan opiskelijoita näkemään, miten graafinen ohjelma luodaan sekä valmentaa heitä ymmärtämään viitekehyksien ja graafisten kirjastojen tuomat edut.

Young Registered Nurses’ Intent to Leave the Profession in Finland - A Mixed-Method Study

The purpose of this study was to examine and expand understanding concerning young Finnish registered nurses (RN) with an intention to leave the profession and the related variables, specifically when that intention has emerged before the age of 30. The overall goal of the study was to develop a conceptual model in relation to young RNs’ intention to leave the profession. Suggestions for policymakers, nurse leaders and nurse managers are presented for how to retain more young RNs in the nursing workforce. Suggestions for future nursing research are also provided. Phase I consists of two sequential integrative literature reviews of 75 empirical articles concerning nurses’ intention to leave the profession. In phase II, data had been collected as part of the Nurses’ Early Exit (NEXT) study, using the BQ-12 structured postal questionnaire. A total of 147 young RNs participated in the study. The data were analysed with statistical methods. In phase III, firstly, an in-depth interpretive case study was conducted in order to understand how young RNs explain and make sense of their intention to leave the profession. The data in this study consisted of longitudinal career stories by three young RNs. The data was analysed by using narrative holistic-content and thematic methods. Secondly, a total of 15 young RNs were interviewed in order to explore in-depth their experiences concerning organizational turnover and their intent to leave the profession. The data was analysed using conventional content analysis. Based on earlier research, empirical research on the young RNs intention to leave the profession is scarce. Nurses’ intention to leave the profession has mainly been studied with quantitative descriptive studies, conducted with survey questionnaires. Furthermore, the quality of previous studies varies considerably. Moreover, nurses’ intention to leave the profession seems to be driven by a number of variables. According to the survey study, 26% of young RNs had often considered giving up nursing completely and starting a different kind of job during the course of the previous year. Many different variables were associated with an intention to leave the profession (e.g. personal burnout, job dissatisfaction). According to the in-depth inquiries, poor nursing practice environments and a nursing career as a ‘second-best’ or serendipitous career choice were themes associated with young RNs’ intention to leave the profession. In summary, young RNs intention to leave the profession is a complex phenomenon with multiple associated variables. These findings suggest that policymakers, nurse leaders and nurse managers should enable improvements in nursing practice environments in order to retain more young RNs. These improvements can include, for example, adequate staffing levels, balanced nursing workloads, measures to reduce work-related stress as well as possibilities for advancement and development. Young RNs’ requirements to provide high-quality and ethical nursing care must be recognized in society and health-care organizations. Moreover, sufficient mentoring and orientation programmes should be provided for all graduate RNs. Future research is needed into whether the motive for choosing a nursing career affects the length of the tenure in the profession. Both quantitative and in-depth research is needed for the comprehensive development of nursing-turnover research.

Developing an introductory object-oriented programming course

The state of the object-oriented programming course in Lappeenranta University of Technology had reached the point, where it required changes to provide better learning opportunities and thus the learning outcomes. Based on the student feedback the course was partially dated and ineffective. The components of the course were analysed and the ineffective elements were removed and new methods were introduced to improve the course. The major changes included the change from traditional teaching methods to reverse classroom method and the use of Java as the programming language. The changes were measured by the student feedback, lecturer’s observations and comparison to previous years. The feedback suggested that the changes were successful; the course received higher overall grade than before.

Open source solutions for multiplatform graphics programming

New emerging technologies in the recent decade have brought new options to cross platform computer graphics development. This master thesis took a look for cross platform 3D graphics development possibilities. All platform dependent and non real time solutions were excluded. WebGL and two different OpenGL based solutions were assessed via demo application by using most recent development tools. In the results pros and cons of the each solutions were noted.