@phdthesis{Yao20GuardBasedSynchronization,
	type = {{PhD} {Thesis}},
	title = {An {Efficient} {Implementation} of {Guard}-based {Synchronization} for an {Object}-{Oriented} {Programming} {Language}},
	url = {http://hdl.handle.net/11375/25567},
	abstract = {Object-oriented programming has had a significant impact on software development because it provides programmers with a clear structure of a large system. It encapsulates data and operations into objects, groups objects into classes and dynamically binds operations to program code. With the emergence of multi-core processors, application developers have to explore concurrent programming to take full advantage of multi-core technology. However, when it comes to concurrent programming, object-oriented programming remains elusive as a useful programming tool. Most object-oriented programming languages do have some extensions for concurrency, but concurrency is implemented independently of objects: for example, concurrency in Java is managed separately with the Thread object. We employ a programming model called Lime that combines action systems tightly with object-oriented programming and implements concurrency by extending classes with actions and guarded methods. This provides programmers with a unified and straightforward design view for a concurrent object-oriented program. In this work, using coroutines with guarded methods and actions is proposed as a means of implementing the concurrency extension for objects. Mapping objects to coroutines can result in stack overflow as the number of objects increases. A dynamically segmented stack mechanism, which does not introduce runtime overhead, is implemented to support large-scale concurrency. Since Lime allows guarded methods and actions to "get stuck," a new user-level cooperative scheduler, and a fast coroutine context switch mechanism are implemented to improve the performance. Compared with the traditional segmented stack mechanisms, the new dynamically segmented stack mechanism gets equal performance for more common scenarios. Besides, it outperforms the contemporary stack mechanisms for deep recursion scenarios. Above all, Lime does not only provide the programmers with a unified and straightforward object-oriented programming model for concurrency, but also accomplishes a better performance than concurrent programming languages such as Erlang and Go, in fine-grained, highly concurrent benchmarks.},
	school = {McMaster University},
	author = {Yao, Shucai},
	month = jul,
	year = {2020},
}

Object-oriented programming has had a significant impact on software development because it provides programmers with a clear structure of a large system. It encapsulates data and operations into objects, groups objects into classes and dynamically binds operations to program code. With the emergence of multi-core processors, application developers have to explore concurrent programming to take full advantage of multi-core technology. However, when it comes to concurrent programming, object-oriented programming remains elusive as a useful programming tool. Most object-oriented programming languages do have some extensions for concurrency, but concurrency is implemented independently of objects: for example, concurrency in Java is managed separately with the Thread object. We employ a programming model called Lime that combines action systems tightly with object-oriented programming and implements concurrency by extending classes with actions and guarded methods. This provides programmers with a unified and straightforward design view for a concurrent object-oriented program. In this work, using coroutines with guarded methods and actions is proposed as a means of implementing the concurrency extension for objects. Mapping objects to coroutines can result in stack overflow as the number of objects increases. A dynamically segmented stack mechanism, which does not introduce runtime overhead, is implemented to support large-scale concurrency. Since Lime allows guarded methods and actions to "get stuck," a new user-level cooperative scheduler, and a fast coroutine context switch mechanism are implemented to improve the performance. Compared with the traditional segmented stack mechanisms, the new dynamically segmented stack mechanism gets equal performance for more common scenarios. Besides, it outperforms the contemporary stack mechanisms for deep recursion scenarios. Above all, Lime does not only provide the programmers with a unified and straightforward object-oriented programming model for concurrency, but also accomplishes a better performance than concurrent programming languages such as Erlang and Go, in fine-grained, highly concurrent benchmarks.

@mastersthesis{Wang19MachineLearningWaterQuality,
	address = {Hamilton, Ontario, Canada},
	title = {Evaluation of {Machine} {Learning}-based {Methods} for {Continuous} {Water} {Quality} {Data} {Analysis}},
	url = {http://hdl.handle.net/11375/24680},
	abstract = {Wastewater treatment facilities are increasingly installing sensors to monitor water quality. As these datasets have increased in size and complexity, it has become difficult to identify abnormal readings in a timely manner either manually or using simple rules that might have been sufficient previously. Two ammonia sensors were installed at the Dundas Wastewater Treatment Plant in November 2017. The collected ammonia concentration data shows a daily pattern. A learning-based method is implemented in this thesis to identify any readings which violate this daily pattern. The data points which were predicted to be anomalous were qualitatively ranked based on the severity and the likelihood of being faulty. The result of the learning-based method was evaluated and compared to other traditional detection methods.},
	school = {McMaster University, Department of Computing and Software},
	author = {Wang, Xi},
	month = apr,
	year = {2019},
}

Wastewater treatment facilities are increasingly installing sensors to monitor water quality. As these datasets have increased in size and complexity, it has become difficult to identify abnormal readings in a timely manner either manually or using simple rules that might have been sufficient previously. Two ammonia sensors were installed at the Dundas Wastewater Treatment Plant in November 2017. The collected ammonia concentration data shows a daily pattern. A learning-based method is implemented in this thesis to identify any readings which violate this daily pattern. The data points which were predicted to be anomalous were qualitatively ranked based on the severity and the likelihood of being faulty. The result of the learning-based method was evaluated and compared to other traditional detection methods.

@mastersthesis{Fadhel19AutomaticCodeReviews,
	address = {Hamilton, Ontario, Canada},
	title = {Towards {Automating} {Code} {Reviews}},
	url = {http://hdl.handle.net/11375/25269},
	abstract = {Existing software engineering tools have proved useful in automating some aspects of the code review process, from uncovering defects to refactoring code. However, given that software teams still spend large amounts of time performing code reviews despite the use of such tools, much more research remains to be carried out in this area. This dissertation present two major contributions to this field. First, we perform a text classification experiment over thirty thousand GitHub review comments to understand what code reviewers typically discuss in reviews. Next, in an attempt to offer an innovative, data-driven approach to automating code reviews, we leverage probabilistic models of source code and graph embedding techniques to perform human-like code inspections. Our experimental results indicate that the proposed algorithm is able to emulate human-like code inspection behaviour in code reviews with a macro f1-score of 62\%, representing an impressive contribution towards the relatively unexplored research domain of automated code reviewing tools.},
	school = {McMaster University},
	author = {Fadhel, Muntazir},
	month = nov,
	year = {2019},
}

Existing software engineering tools have proved useful in automating some aspects of the code review process, from uncovering defects to refactoring code. However, given that software teams still spend large amounts of time performing code reviews despite the use of such tools, much more research remains to be carried out in this area. This dissertation present two major contributions to this field. First, we perform a text classification experiment over thirty thousand GitHub review comments to understand what code reviewers typically discuss in reviews. Next, in an attempt to offer an innovative, data-driven approach to automating code reviews, we leverage probabilistic models of source code and graph embedding techniques to perform human-like code inspections. Our experimental results indicate that the proposed algorithm is able to emulate human-like code inspection behaviour in code reviews with a macro f1-score of 62%, representing an impressive contribution towards the relatively unexplored research domain of automated code reviewing tools.

@phdthesis{Burton18DynamicMixins,
	address = {Hamilton, Ontario, Canada},
	type = {Ph.{D}. {Thesis}},
	title = {Using {Dynamic} {Mixins} for {Software} {Development}},
	url = {http://hdl.handle.net/11375/23829},
	abstract = {Object-oriented programming has gained significant traction in the software development community and is now the common approach for developing large, commercial applications. Many of these applications require the behaviour of objects to be modified at run-time. Contemporary class-based, statically-typed languages such as C++ and Java require collaboration with external objects to modify an object’s behaviour. Furthermore, such an object must be designed to order to support such collaborations. Dynamic languages such as Python which natively support object extension do not guarantee type safety. In this work, using dynamic mixins with static typing is proposed as a means of providing type-safe, object extension. A new language called mix is introduced that allows a compiler to syntactically check the type-safety of an object extension. A model to support object-oriented development is extended to support dynamic mixins. The utility of the approach is illustrated using sample use cases. Finally, a compiler was implemented to validate the practicality of the model proposed.},
	school = {McMaster University},
	author = {Burton, Ronald},
	month = jul,
	year = {2018},
}

Object-oriented programming has gained significant traction in the software development community and is now the common approach for developing large, commercial applications. Many of these applications require the behaviour of objects to be modified at run-time. Contemporary class-based, statically-typed languages such as C++ and Java require collaboration with external objects to modify an object’s behaviour. Furthermore, such an object must be designed to order to support such collaborations. Dynamic languages such as Python which natively support object extension do not guarantee type safety. In this work, using dynamic mixins with static typing is proposed as a means of providing type-safe, object extension. A new language called mix is introduced that allows a compiler to syntactically check the type-safety of an object extension. A model to support object-oriented development is extended to support dynamic mixins. The utility of the approach is illustrated using sample use cases. Finally, a compiler was implemented to validate the practicality of the model proposed.

@phdthesis{Nokovic16HighLevelModels,
	address = {Hamilton, Ontario, Canada},
	type = {Ph.{D}. {Thesis}},
	title = {Verification and {Implementation} of {Embedded} {Systems} from {High}-{Level} {Models}},
	url = {http://hdl.handle.net/11375/19169},
	abstract = {Existing modelling tools for embedded systems analyze models that do not necessarily reflect executable code. We propose a holistic approach that includes visual modelling of the system and its environment, qualitative and quantitative verification of the model, and automated executable code generation. 

For high-level modelling, we introduce pCharts, a variant of hierarchical state machines with state invariants, probabilistic transitions, timed transitions, stochastic transitions, state costs, and transition costs. With embedded systems in mind, pCharts follow an event-centric interpretation, in which events are executable procedures, implying that their execution is fast enough that no queuing of events is needed. 

Our pCharts tool, pState, allows the whole system to be formally analyzed and code for executable parts generated. The goal is an automated approach from modelling and analysis to code generation. On a series of case studies, we demonstrate this technique.

An off-the-shelf probabilistic model checker is used for analysis by compiling and transforming a hierarchical pCharts into a flat collection of probabilistic guarded commands with costs. From the pCharts model, also executable code that preserves the verified properties can be generated.},
	school = {McMaster University},
	author = {Nokovic, Bojan},
	month = mar,
	year = {2016},
}

Existing modelling tools for embedded systems analyze models that do not necessarily reflect executable code. We propose a holistic approach that includes visual modelling of the system and its environment, qualitative and quantitative verification of the model, and automated executable code generation. For high-level modelling, we introduce pCharts, a variant of hierarchical state machines with state invariants, probabilistic transitions, timed transitions, stochastic transitions, state costs, and transition costs. With embedded systems in mind, pCharts follow an event-centric interpretation, in which events are executable procedures, implying that their execution is fast enough that no queuing of events is needed. Our pCharts tool, pState, allows the whole system to be formally analyzed and code for executable parts generated. The goal is an automated approach from modelling and analysis to code generation. On a series of case studies, we demonstrate this technique. An off-the-shelf probabilistic model checker is used for analysis by compiling and transforming a hierarchical pCharts into a flat collection of probabilistic guarded commands with costs. From the pCharts model, also executable code that preserves the verified properties can be generated.

@phdthesis{zhang_unifying_2013,
	address = {Hamilton, Ontario, Canada},
	type = {Ph.{D}. {Thesis}},
	title = {A {Unifying} {Theory} of {Multi}-{Exit} {Programs}},
	url = {http://hdl.handle.net/11375/13534},
	abstract = {Programs have multiple exits in the presence of certain control structures, e.g., exception handling and coroutines. These control structures offer flexible manipulations of control flow. However, their formalizations are overall specialized, which hinders reasoning about combinations of these control structures.

In this thesis, we propose a unifying theory of multi-exit programs. We mechanically formalize the semantics of multi-exit programs as indexed predicate transformers, a generalization of predicate transformers by taking the tuple of postconditions on all exits as the parameter. We explore their algebraic properties and verification rules, then define a normal form for monotonic and for conjunctive indexed predicate transformers. We also propose a new notion of fail-safe correctness to model the category of programs that always maintain certain safe conditions when they fail, and a new notion of fail-safe refinement to express partiality in software development.

For the indexed predicate transformer formalization, we illustrate its applications in three models of multi-exit control structures: the termination model of exception handling, the retry model of exception handling, and a coroutine model. Additionally, for the fail-safe correctness notion and the fail-safe refinement notion, we illustrate their applications in the termination model. Six design patterns in the termination model and one in the retry model are studied. All the verification rules and design patterns in the thesis have been formally checked by a verification tool.},
	school = {McMaster University},
	author = {Zhang, Tian},
	month = sep,
	year = {2013},
}

Programs have multiple exits in the presence of certain control structures, e.g., exception handling and coroutines. These control structures offer flexible manipulations of control flow. However, their formalizations are overall specialized, which hinders reasoning about combinations of these control structures. In this thesis, we propose a unifying theory of multi-exit programs. We mechanically formalize the semantics of multi-exit programs as indexed predicate transformers, a generalization of predicate transformers by taking the tuple of postconditions on all exits as the parameter. We explore their algebraic properties and verification rules, then define a normal form for monotonic and for conjunctive indexed predicate transformers. We also propose a new notion of fail-safe correctness to model the category of programs that always maintain certain safe conditions when they fail, and a new notion of fail-safe refinement to express partiality in software development. For the indexed predicate transformer formalization, we illustrate its applications in three models of multi-exit control structures: the termination model of exception handling, the retry model of exception handling, and a coroutine model. Additionally, for the fail-safe correctness notion and the fail-safe refinement notion, we illustrate their applications in the termination model. Six design patterns in the termination model and one in the retry model are studied. All the verification rules and design patterns in the thesis have been formally checked by a verification tool.

@mastersthesis{moore-oliva_comparison_2010,
	address = {Hamilton, Ontario, Canada},
	title = {A {Comparison} of {Scalable} {Multi}-{Threaded} {Stack} {Mechanisms}},
	url = {http://hdl.handle.net/11375/9011},
	abstract = {The traditional "stack grows from the top, heap grows from the bottom" memory layout allows a single-threaded process to make use of all available address space. This layout is not ideal when multiple threads of execution need to share one address space, for memory exhaustion is no longer signified by the heap meeting the stack. In the commonly used multi-threaded memory layout where each thread has its "worst case" stack memory exclusively reserved, a process may prematurely run out of memory when one thread's stack collides with another's, even if there is unused address space elsewhere. This problem is exacerbated as the number of threads in a process increases since there is less stack space available per thread. In this thesis, alternative stack mechanisms that attempt to alleviate this problem are reviewed, and a new stack mechanism is put forward that utilizes the MMU to detect stack overflow. An experimental compiler implementing a subset of the C language is used to implement promising stack mechanisms, and a suite of test programs are used to compare their performance and scalability under varying usage patterns.},
	school = {McMaster University},
	author = {Moore-Oliva, Joshua I.},
	month = dec,
	year = {2010},
}

The traditional "stack grows from the top, heap grows from the bottom" memory layout allows a single-threaded process to make use of all available address space. This layout is not ideal when multiple threads of execution need to share one address space, for memory exhaustion is no longer signified by the heap meeting the stack. In the commonly used multi-threaded memory layout where each thread has its "worst case" stack memory exclusively reserved, a process may prematurely run out of memory when one thread's stack collides with another's, even if there is unused address space elsewhere. This problem is exacerbated as the number of threads in a process increases since there is less stack space available per thread. In this thesis, alternative stack mechanisms that attempt to alleviate this problem are reviewed, and a new stack mechanism is put forward that utilizes the MMU to detect stack overflow. An experimental compiler implementing a subset of the C language is used to implement promising stack mechanisms, and a suite of test programs are used to compare their performance and scalability under varying usage patterns.

@mastersthesis{cui09ABC,
	address = {Hamilton, Ontario, Canada},
	title = {An {Experimental} {Implementation} of {Action}-{Based} {Concurrency}},
	url = {http://hdl.handle.net/11375/21409},
	abstract = {This thesis reports on an implementation of an action-based model for concurrent
 programming. Concurrency is expressed by allowing objects to have actions with a guard and a body. Each action has its own execution context, and concurrent execution is realized when program execution is happening in more than one context at a time. Two actions of different objects can run concurrently, and they are synchronized whenever a shared object is accessed simultaneously by both actions. The appeal of this model is that it allows a conceptually simple framework for designing and analyzing concurrent programs.

To experiment with action-based concurrency, we present a small language, ABC Pascal, which is an experimental attempt as a proof of feasibility of such a model, and also meant to help identify issues for achieving reasonable efficiency in implementation. It extends a subset of Pascal that supports basic sequential programming constructs, and provides action-based concurrency as the action-based model prescribes.

This work deals with the specification and implementation of ABC Pascal. The one-pass compiler directly generates assembly code, without devoting efforts to optimization. While the code is not optimized, the results that ABC Pascal has achieved in performance testing are so far comparable to mainstream concurrent programming languages.},
	school = {McMaster University},
	author = {Cui, Xiao-lei},
	month = jan,
	year = {2009},
}

This thesis reports on an implementation of an action-based model for concurrent programming. Concurrency is expressed by allowing objects to have actions with a guard and a body. Each action has its own execution context, and concurrent execution is realized when program execution is happening in more than one context at a time. Two actions of different objects can run concurrently, and they are synchronized whenever a shared object is accessed simultaneously by both actions. The appeal of this model is that it allows a conceptually simple framework for designing and analyzing concurrent programs. To experiment with action-based concurrency, we present a small language, ABC Pascal, which is an experimental attempt as a proof of feasibility of such a model, and also meant to help identify issues for achieving reasonable efficiency in implementation. It extends a subset of Pascal that supports basic sequential programming constructs, and provides action-based concurrency as the action-based model prescribes. This work deals with the specification and implementation of ABC Pascal. The one-pass compiler directly generates assembly code, without devoting efforts to optimization. While the code is not optimized, the results that ABC Pascal has achieved in performance testing are so far comparable to mainstream concurrent programming languages.

@mastersthesis{kelk_formal_2009,
	address = {Hamilton, Ontario, Canada},
	title = {Formal {Modelling} of {Version} {Control} {Systems}},
	url = {http://hdl.handle.net/11375/9114},
	abstract = {Version control systems are widely used to manage collections of files and directories, along with changes made to them over their lifetime. Any previously checked in version of a file is recoverable at any time from the repository. They allow people to work on the same files in a decentralized and concurrent way, while consistently managing and integrating changes. In this thesis we develop a subset of the SVN and CVS version control systems from specifications using Atelier B 4. Both of these systems are feature rich, widely used in cross-platform environments and representative of their class of file based extensional version control systems. Support for abstract data types like sets and refinement is well suited to the task. The most commonly used features such as Add, Check-in, Update are modeled in increasing detail in multiple refinement steps. Later refinement steps add features such as binary file support and the local cache. Having both models allows us to compare and contrast their feature sets. Documentation for SVN and CVS is extensive but informal. One feature of CVS required experimentation when the written documentation was insufficient. SVN is modelled in approximately 1400 lines in eight refinement steps with 109 proof obligations. CVS is likewise specified in roughly 1150 lines in seven steps with 29 proof obligations. With all proof obligations discharged we are confident the models represent the real systems and are a reasonable first step towards the goal of verifiable implementations of version control systems.},
	school = {McMaster University},
	author = {Kelk, David},
	month = dec,
	year = {2009},
}

Version control systems are widely used to manage collections of files and directories, along with changes made to them over their lifetime. Any previously checked in version of a file is recoverable at any time from the repository. They allow people to work on the same files in a decentralized and concurrent way, while consistently managing and integrating changes. In this thesis we develop a subset of the SVN and CVS version control systems from specifications using Atelier B 4. Both of these systems are feature rich, widely used in cross-platform environments and representative of their class of file based extensional version control systems. Support for abstract data types like sets and refinement is well suited to the task. The most commonly used features such as Add, Check-in, Update are modeled in increasing detail in multiple refinement steps. Later refinement steps add features such as binary file support and the local cache. Having both models allows us to compare and contrast their feature sets. Documentation for SVN and CVS is extensive but informal. One feature of CVS required experimentation when the written documentation was insufficient. SVN is modelled in approximately 1400 lines in eight refinement steps with 109 proof obligations. CVS is likewise specified in roughly 1150 lines in seven steps with 29 proof obligations. With all proof obligations discharged we are confident the models represent the real systems and are a reasonable first step towards the goal of verifiable implementations of version control systems.

@mastersthesis{pujari_verification_2009,
	address = {Hamilton, Ontario, Canada},
	title = {Verification and {Refinement} {Theory} of {Action} {Inheritance} for {Concurrent} {Objects}},
	url = {http://hdl.handle.net/11375/9157},
	abstract = {Lime is an action-based concurrent object-oriented programming language. Lime treats concurrency and object-orientation as a single concern and encapsulates concurrent features within objects. In Lime objects, concurrency is expressed with guarded methods and actions. Inheritance is a characteristic feature of object-oriented programming languages. Lime supports inheritance of methods. In this thesis we extend class inheritance in Lime to include inheritance of actions. This ensures that autonomous behavior of the class is also inherited. Class inheritance also aids in verification and refinement of classes. We establish class refinement rules for class inheritance. When these rules are satisfied, the subclass is a subtype as well as a refinement of the parent class. Lime uses modules as a means to define classes in terms of action systems. In our research, we extend the modules to support class inheritance. In this extended form, class modularization is useful for verification and class refinement. Concurrent object-oriented programming languages are affected by the Inheritance Anomaly - a conflict between inheritance and concurrency. We show that Lime's support for atomicity of methods and actions up to method calls allows our model of classes' inheritance to avoid the problem of the Inheritance Anomaly.},
	school = {McMaster University},
	author = {Pujari, Upasana},
	month = sep,
	year = {2009},
}

Lime is an action-based concurrent object-oriented programming language. Lime treats concurrency and object-orientation as a single concern and encapsulates concurrent features within objects. In Lime objects, concurrency is expressed with guarded methods and actions. Inheritance is a characteristic feature of object-oriented programming languages. Lime supports inheritance of methods. In this thesis we extend class inheritance in Lime to include inheritance of actions. This ensures that autonomous behavior of the class is also inherited. Class inheritance also aids in verification and refinement of classes. We establish class refinement rules for class inheritance. When these rules are satisfied, the subclass is a subtype as well as a refinement of the parent class. Lime uses modules as a means to define classes in terms of action systems. In our research, we extend the modules to support class inheritance. In this extended form, class modularization is useful for verification and class refinement. Concurrent object-oriented programming languages are affected by the Inheritance Anomaly - a conflict between inheritance and concurrency. We show that Lime's support for atomicity of methods and actions up to method calls allows our model of classes' inheritance to avoid the problem of the Inheritance Anomaly.

@mastersthesis{zhou_implementation_2007,
	address = {Hamilton, Ontario, Canada},
	title = {Implementation of {Tabular} {Verification} and {Refinement}},
	url = {http://hdl.handle.net/11375/21116},
	abstract = {It has been argued for some time that tabular representations of formal specifications can help in writing them, in understanding them, and in checking them. Recently it has been suggested that tabular representations also help in breaking down large verification and refinement conditions into a number of smaller ones.

The article [32] developed the theory, but the real proof in terms of an implementation is not provided. This project is about formalizing tables in a theorem prover, Simplify, defining theorems of [32] in terms of functions written in the OCaml programming language, and conducting some case studies in verifying and refining realistic problems.

A parser is designed to ease our job of inputting expressions. Pretty-print is also provided: all predicates and tables of the examples in our thesis are automatically generated.

Our first example is a control system, a luxury sedan car seat. This example gives us an overall impression on how to prove correctness from tabular specification. The second example specifies a visitor information system. The design features of this example involve modeling properties and operations on sets, relations and functions by building self-defined axioms. The third example illustrates another control system, an elevator. Theorems of algorithmic refinements, stepwise data refinements, and the combination of algorithmic abstraction and data abstraction are applied correspondingly to different operations.},
	school = {McMaster University},
	author = {Zhou, Ning},
	month = feb,
	year = {2007},
}

It has been argued for some time that tabular representations of formal specifications can help in writing them, in understanding them, and in checking them. Recently it has been suggested that tabular representations also help in breaking down large verification and refinement conditions into a number of smaller ones. The article [32] developed the theory, but the real proof in terms of an implementation is not provided. This project is about formalizing tables in a theorem prover, Simplify, defining theorems of [32] in terms of functions written in the OCaml programming language, and conducting some case studies in verifying and refining realistic problems. A parser is designed to ease our job of inputting expressions. Pretty-print is also provided: all predicates and tables of the examples in our thesis are automatically generated. Our first example is a control system, a luxury sedan car seat. This example gives us an overall impression on how to prove correctness from tabular specification. The second example specifies a visitor information system. The design features of this example involve modeling properties and operations on sets, relations and functions by building self-defined axioms. The third example illustrates another control system, an elevator. Theorems of algorithmic refinements, stepwise data refinements, and the combination of algorithmic abstraction and data abstraction are applied correspondingly to different operations.

@mastersthesis{zingaro_practice_2007,
	address = {Hamilton, Ontario, Canada},
	title = {On the {Practice} of {B}-ing {Earley}},
	url = {http://hdl.handle.net/11375/21372},
	abstract = {arley's parsing algorithm is an O(n{\textasciicircum}3) algorithm for parsing according to any context-free grammar. Its theoretical importance stems from the fact that it was one of the first algorithms to achieve this time bound, but it has also seen success in compiler-compilers, theorem provers and natural language processing. It has an elegant structure, and its time complexity on restricted classes of grammars is often as good as specialized algorithms. Grammars with ϵ-productions, however, require special consideration, and have historically lead to inefficient and inelegant implementations.

In this thesis, we develop the algorithm from specification using the B-Method. Through refinement steps, we arrive at a list-processing formulation, in which the problems with ϵ-productions emerge and can be understood. The development highlights the essential properties of the algorithm, and has also lead to the discovery of an implementation optimization. We end by giving a concept-test of the algorithm as a literate Pascal program.},
	school = {McMaster University},
	author = {Zingaro, Daniel},
	month = aug,
	year = {2007},
}

arley's parsing algorithm is an O(n\textasciicircum3) algorithm for parsing according to any context-free grammar. Its theoretical importance stems from the fact that it was one of the first algorithms to achieve this time bound, but it has also seen success in compiler-compilers, theorem provers and natural language processing. It has an elegant structure, and its time complexity on restricted classes of grammars is often as good as specialized algorithms. Grammars with ϵ-productions, however, require special consideration, and have historically lead to inefficient and inelegant implementations. In this thesis, we develop the algorithm from specification using the B-Method. Through refinement steps, we arrive at a list-processing formulation, in which the problems with ϵ-productions emerge and can be understood. The development highlights the essential properties of the algorithm, and has also lead to the discovery of an implementation optimization. We end by giving a concept-test of the algorithm as a literate Pascal program.

@mastersthesis{zhao_object-oriented_2007,
	address = {Hamilton, Ontario, Canada},
	title = {Object-{Oriented} {Literate} {Programming}},
	url = {http://hdl.handle.net/11375/21290},
	abstract = {During the past decades, programming methodology has seen an improvement by
 structured programming and object-oriented programming (OOP), leading to software
 that is more reliable and easier to develop. However, software engineers are still
 dealing with problems in processing associated documentation. Literate programming
 was introduced by Donald Knuth in the early 80's as an approach to produce programs
 together with their documentation in a way that is aimed at consumption by
 humans rather than by compilers. However, dated and complex features, dependence
 on formatting and programming language, and a lack of methodology prevented the
 method from gaining in popularity.

In this thesis, we propose an approach to "integrate" OOP with literate programming
 in order to present and document the whole design in a consistent and
 maintainable way. In our approach, both program code and corresponding documentation
 are generated from the same source. The resulting documentation consists
 of code chunks with detailed explanations, as well as automatically generated class
 diagrams with varying levels of detail. A tool, Spark, has been developed and applied
 to the design of a Transit Information System from requirement analysis to testing.
 Spark was also used in its own development.},
	school = {McMaster University},
	author = {Zhao, Ming Yu},
	month = aug,
	year = {2007},
}

During the past decades, programming methodology has seen an improvement by structured programming and object-oriented programming (OOP), leading to software that is more reliable and easier to develop. However, software engineers are still dealing with problems in processing associated documentation. Literate programming was introduced by Donald Knuth in the early 80's as an approach to produce programs together with their documentation in a way that is aimed at consumption by humans rather than by compilers. However, dated and complex features, dependence on formatting and programming language, and a lack of methodology prevented the method from gaining in popularity. In this thesis, we propose an approach to "integrate" OOP with literate programming in order to present and document the whole design in a consistent and maintainable way. In our approach, both program code and corresponding documentation are generated from the same source. The resulting documentation consists of code chunks with detailed explanations, as well as automatically generated class diagrams with varying levels of detail. A tool, Spark, has been developed and applied to the design of a Transit Information System from requirement analysis to testing. Spark was also used in its own development.

@mastersthesis{lou_compiler_2004,
	address = {Hamilton, Ontario, Canada},
	title = {A {Compiler} for an {Action}-{Based} {Object}-{Oriented} {Programming} {Language}},
	url = {http://www.cas.mcmaster.ca/~emil/pubs/Lou04ActionOOPL.pdf},
	abstract = {Lime is an action-based object-oriented concurrent programming language, which was developed by Dr. Sekerinski from McMaster University. The development of Lime is based on the observation that more and more applications will be implemented on networks of processors in the future and those are significantly more ambitious than current applications. It is difficult for programmers to do multiprogramming using current object-oriented programming languages. Action systems, which model concurrency by nondeterministic choice among atomic actions (e.g. Lamport’s Temporal Logic of Actions, J. Misra and K. M. Chandy’s Unity Logic and Back’s Action Systems), can help us to simplify both the specification and design of concurrent applications. But all of that is still theoretical. Such action systems have not been implemented and experimented with very thoroughly.

Lime is an object-oriented programming language that is based on the action system. The closest approach is Seuss, which was developed by J. Misra et.al. at The University of Texas at Austin, but the limitation of Seuss is that it is not fully object-oriented. One purpose of my research is to find out how to schedule actions for applications running on a multiprocessor environment. I implemented a compiler for this new technique that can translate programs written in Lime to Java assembly language.

Object-oriented programming techniques are used widely in software development, and Lime can make a good combination of these techniques and action systems. So we can make the development of object-oriented concurrent programs much easier and efficient.},
	school = {McMaster University},
	author = {Lou, Kevin},
	year = {2004},
}

Lime is an action-based object-oriented concurrent programming language, which was developed by Dr. Sekerinski from McMaster University. The development of Lime is based on the observation that more and more applications will be implemented on networks of processors in the future and those are significantly more ambitious than current applications. It is difficult for programmers to do multiprogramming using current object-oriented programming languages. Action systems, which model concurrency by nondeterministic choice among atomic actions (e.g. Lamport’s Temporal Logic of Actions, J. Misra and K. M. Chandy’s Unity Logic and Back’s Action Systems), can help us to simplify both the specification and design of concurrent applications. But all of that is still theoretical. Such action systems have not been implemented and experimented with very thoroughly. Lime is an object-oriented programming language that is based on the action system. The closest approach is Seuss, which was developed by J. Misra et.al. at The University of Texas at Austin, but the limitation of Seuss is that it is not fully object-oriented. One purpose of my research is to find out how to schedule actions for applications running on a multiprocessor environment. I implemented a compiler for this new technique that can translate programs written in Lime to Java assembly language. Object-oriented programming techniques are used widely in software development, and Lime can make a good combination of these techniques and action systems. So we can make the development of object-oriented concurrent programs much easier and efficient.

@mastersthesis{shalaby_formal_2004,
	address = {Hamilton, Ontario, Canada},
	title = {Formal {Analysis} of {Invariant}-{Based} {Design} {Patterns}},
	url = {http://www.cas.mcmaster.ca/~emil/pubs/Shalaby04InvariantDesignPatterns.pdf},
	abstract = {This study introduces a formal abstract notation to describe precisely structural and behavioral aspects of design patterns. A pattern description is constructed based on the book of Gamma et al., and is refined through analyzing carefully selected example implementations. Example implementations come from existing large real-world programs. Produced pattern descriptions can be used to check the compliance of other instances with intended patterns.

It is also shown that for some patterns, even the combined structural and behavioral descriptions are not enough to capture the essence of a pattern. An invariant has to be introduced to complement the pattern description. Based on components needed to describe patterns, they can be classified into structure-based patterns, behavior-based patterns, and invariant-based patterns. The latest require the most comprehensive description and are the focus of this study.

As a very detail-rich pattern, Iterator is selected as an example to apply the complete process on it. Invariants are also introduced for three other patterns to show that the need for invariants is not limited to one pattern.

The study shows that differentiating design patterns in their formal abstract notation is easier and more precise than when done based on class diagrams and natural language descriptions. Also, the process of establishing a pattern description can itself give a better insight about the essence and details of the described pattern.},
	school = {McMaster University},
	author = {Shalaby, Hany},
	month = jun,
	year = {2004},
}

This study introduces a formal abstract notation to describe precisely structural and behavioral aspects of design patterns. A pattern description is constructed based on the book of Gamma et al., and is refined through analyzing carefully selected example implementations. Example implementations come from existing large real-world programs. Produced pattern descriptions can be used to check the compliance of other instances with intended patterns. It is also shown that for some patterns, even the combined structural and behavioral descriptions are not enough to capture the essence of a pattern. An invariant has to be introduced to complement the pattern description. Based on components needed to describe patterns, they can be classified into structure-based patterns, behavior-based patterns, and invariant-based patterns. The latest require the most comprehensive description and are the focus of this study. As a very detail-rich pattern, Iterator is selected as an example to apply the complete process on it. Invariants are also introduced for three other patterns to show that the need for invariants is not limited to one pattern. The study shows that differentiating design patterns in their formal abstract notation is easier and more precise than when done based on class diagrams and natural language descriptions. Also, the process of establishing a pattern description can itself give a better insight about the essence and details of the described pattern.

@mastersthesis{liang_inheritance_2004,
	address = {Hamilton, Ontario, Canada},
	title = {Inheritance, {Specification} and {Documentation} {Support} for an {Object}-{Oriented} {Language}},
	url = {http://www.cas.mcmaster.ca/~emil/pubs/Liang04InheritSpecDocForOO.pdf},
	abstract = {Lime is an object-oriented programming language with action-based concurrency. Concurrency in Lime has been previously implemented. Our current work integrates specification and documentation features into Lime and its compiler. The goal of this integration is to improve software quality, in particular correctness, extensibility, and maintainability in a uniform and coherent manner. Lime provides a flexible inheritance mechanism that separates subclassing (code sharing) from subtyping (substitutability). Any class can sever as a superclass (for the purpose of reuse) or/and as a supertype (for the purpose of specification) and any child class can either inherit the implementation, the interface specification, or both. Behavioral specifications are expressed by preconditions, postconditions and in- variants. These and other intermediate annotations can be written using quantifiers and other standard mathematical notation, and can be checked at run-time. The associated documentation tool generates a description of the behavioral inter- face of each class that includes the preconditions and postconditions of the methods, the class invariants, the subtype hierarchy, and subclass hierarchy.},
	school = {McMaster University},
	author = {Liang, Jie},
	month = aug,
	year = {2004},
}

Lime is an object-oriented programming language with action-based concurrency. Concurrency in Lime has been previously implemented. Our current work integrates specification and documentation features into Lime and its compiler. The goal of this integration is to improve software quality, in particular correctness, extensibility, and maintainability in a uniform and coherent manner. Lime provides a flexible inheritance mechanism that separates subclassing (code sharing) from subtyping (substitutability). Any class can sever as a superclass (for the purpose of reuse) or/and as a supertype (for the purpose of specification) and any child class can either inherit the implementation, the interface specification, or both. Behavioral specifications are expressed by preconditions, postconditions and in- variants. These and other intermediate annotations can be written using quantifiers and other standard mathematical notation, and can be checked at run-time. The associated documentation tool generates a description of the behavioral inter- face of each class that includes the preconditions and postconditions of the methods, the class invariants, the subtype hierarchy, and subclass hierarchy.