--- layout: page title: About Me footer: false --- {% img about-me /images/naorye.jpg me %}
My name is Naor Yehudaey (naorye) and I live in the holy city Jerusalem of Israel.
I am 29 years old, married to my lovely Ilana and we have a female cat named Mutzi.
Since I remember myself I have always had a great passion developing new apps with
thrilling and innovative technologies.
My first big experience was at college, in my seminarion project. Those days
J2ME
was the leading technology for mobile, and I had created an application that allows
sending and receiving emails via mobile phone. This might sound very simple nowadays
but in the middle of 2003, a lot before Android and iPhone were created, when the
leading mobile in the israeli market was
Nokia 3510
it was quite innovative.
Later I understood that mobile apps development is about to change among with the
desktop apps development. More and more apps moved to the cloud and many different
development technologies have arisen. The new invention of
ajax
and its use in GMail (2004) was
a great jump in the web development history that made the JavaScript live again.
Ever since, I dedicate my spare time to learn and developing new web apps, implementing
new ideas and learning the new fascinating possibilities of the web.


{# Home page for a logged in user having role 'user'. #} {% extends "home.html" %} {% block content-left %}


Rails Girls Auckland
4/5 July 2014
|
|
|
|
@NatDudley
|
@mayaneise
|
|
|
|
|
@karrisaarinen
|
@lindaliukas
|
Why Rails Girls Auckland?
About Rails Girls Auckland
Tara Sacha Maia Annette Aurelia Rebecca Molly Elizabeth Grace Madeleine Alysa Nicki Caitlin Georgi Emily Neala Michelle Amie Claire Nicole Angela Carole Lesley Georgina Rebecca Liz Jayne Alice Judy Julia Priya Lena Kerry Laura Corin Min Ha Amy Megan Elora Presley Alexia Michelle Mary Michelle Karin Saboon Raza Sarah Aliya Sarah Catrin
3 photographers
Chris Murat Sim
Bathrooms
Fire Exit
Code of Conduct
Wifi
Coffee, Food and Drinks
Take the Rails Girls Auckland quiz at:
http://goo.gl/foMDXv
We will randomly select 5 winners from the correct answers. Get your answers in by 5.30pm. We will announce the winners before the celebration.


IndPropInductively Defined Propositions
Set Warnings "-notation-overridden,-parsing".
Require Export Logic.
Require Coq.omega.Omega.
Inductively Defined Propositions
- Rule ev_0: The number 0 is even.
- Rule ev_SS: If n is even, then S (S n) is even.
| (ev_0) | |
| ev 0 |
| ev n | (ev_SS) |
| ev (S (S n)) |
------ (ev_0)
ev 0
------ (ev_SS)
ev 2
------ (ev_SS)
ev 4
ev 0
------ (ev_SS)
ev 2
------ (ev_SS)
ev 4
Inductive ev : nat → Prop :=
| ev_0 : ev 0
| ev_SS : ∀ n : nat, ev n → ev (S (S n)).
This definition is different in one crucial respect from
previous uses of Inductive: its result is not a Type, but
rather a function from nat to Prop — that is, a property of
numbers. Note that we've already seen other inductive definitions
that result in functions, such as list, whose type is Type →
Type. What is new here is that, because the nat argument of
ev appears unnamed, to the right of the colon, it is allowed
to take different values in the types of different constructors:
0 in the type of ev_0 and S (S n) in the type of ev_SS.
In contrast, the definition of list names the X parameter
globally, to the left of the colon, forcing the result of
nil and cons to be the same (list X). Had we tried to bring
nat to the left in defining ev, we would have seen an error:
Fail Inductive wrong_ev (n : nat) : Prop :=
| wrong_ev_0 : wrong_ev 0
| wrong_ev_SS : ∀ n, wrong_ev n → wrong_ev (S (S n)).
(* ===> Error: A parameter of an inductive type n is not
allowed to be used as a bound variable in the type
of its constructor. *)
("Parameter" here is Coq jargon for an argument on the left of the
colon in an Inductive definition; "index" is used to refer to
arguments on the right of the colon.)
We can think of the definition of ev as defining a Coq property
ev : nat → Prop, together with theorems ev_0 : ev 0 and
ev_SS : ∀ n, ev n → ev (S (S n)).
Such "constructor theorems" have the same status as proven
theorems. In particular, we can use Coq's apply tactic with the
rule names to prove ev for particular numbers...
Theorem ev_4 : ev 4.
Proof. apply ev_SS. apply ev_SS. apply ev_0. Qed.
... or we can use function application syntax:
Theorem ev_4' : ev 4.
Proof. apply (ev_SS 2 (ev_SS 0 ev_0)). Qed.
We can also prove theorems that have hypotheses involving ev.
Theorem ev_plus4 : ∀ n, ev n → ev (4 + n).
Proof.
intros n. simpl. intros Hn.
apply ev_SS. apply ev_SS. apply Hn.
Qed.
Theorem ev_double : ∀ n,
ev (double n).
Proof.
(* FILL IN HERE *) Admitted.
☐
ev (double n).
Proof.
(* FILL IN HERE *) Admitted.
Using Evidence in Proofs
- E is ev_0 (and n is O), or
- E is ev_SS n' E' (and n is S (S n'), where E' is evidence for ev n').
Inversion on Evidence
- If the evidence is of the form ev_0, we know that n = 0.
- Otherwise, the evidence must have the form ev_SS n' E', where n = S (S n') and E' is evidence for ev n'.
Theorem ev_minus2 : ∀ n,
ev n → ev (pred (pred n)).
Proof.
intros n E.
inversion E as [| n' E'].
- (* E = ev_0 *) simpl. apply ev_0.
- (* E = ev_SS n' E' *) simpl. apply E'. Qed.
In words, here is how the inversion reasoning works in this proof:
This particular proof also works if we replace inversion by
destruct:
- If the evidence is of the form ev_0, we know that n = 0.
Therefore, it suffices to show that ev (pred (pred 0)) holds.
By the definition of pred, this is equivalent to showing that
ev 0 holds, which directly follows from ev_0.
- Otherwise, the evidence must have the form ev_SS n' E', where n = S (S n') and E' is evidence for ev n'. We must then show that ev (pred (pred (S (S n')))) holds, which, after simplification, follows directly from E'.
Theorem ev_minus2' : ∀ n,
ev n → ev (pred (pred n)).
Proof.
intros n E.
destruct E as [| n' E'].
- (* E = ev_0 *) simpl. apply ev_0.
- (* E = ev_SS n' E' *) simpl. apply E'. Qed.
The difference between the two forms is that inversion is more
convenient when used on a hypothesis that consists of an inductive
property applied to a complex expression (as opposed to a single
variable). Here's is a concrete example. Suppose that we wanted
to prove the following variation of ev_minus2:
Theorem evSS_ev : ∀ n,
ev (S (S n)) → ev n.
Intuitively, we know that evidence for the hypothesis cannot
consist just of the ev_0 constructor, since O and S are
different constructors of the type nat; hence, ev_SS is the
only case that applies. Unfortunately, destruct is not smart
enough to realize this, and it still generates two subgoals. Even
worse, in doing so, it keeps the final goal unchanged, failing to
provide any useful information for completing the proof.
Proof.
intros n E.
destruct E as [| n' E'].
- (* E = ev_0. *)
(* We must prove that n is even from no assumptions! *)
Abort.
What happened, exactly? Calling destruct has the effect of
replacing all occurrences of the property argument by the values
that correspond to each constructor. This is enough in the case
of ev_minus2' because that argument, n, is mentioned directly
in the final goal. However, it doesn't help in the case of
evSS_ev since the term that gets replaced (S (S n)) is not
mentioned anywhere.
The inversion tactic, on the other hand, can detect (1) that the
first case does not apply, and (2) that the n' that appears on
the ev_SS case must be the same as n. This allows us to
complete the proof:
Theorem evSS_ev : ∀ n,
ev (S (S n)) → ev n.
Proof.
intros n E.
inversion E as [| n' E'].
(* We are in the E = ev_SS n' E' case now. *)
apply E'.
Qed.
By using inversion, we can also apply the principle of explosion
to "obviously contradictory" hypotheses involving inductive
properties. For example:
Theorem one_not_even : ¬ ev 1.
Proof.
intros H. inversion H. Qed.
Theorem SSSSev__even : ∀ n,
ev (S (S (S (S n)))) → ev n.
Proof.
(* FILL IN HERE *) Admitted.
Theorem even5_nonsense :
ev 5 → 2 + 2 = 9.
Proof.
(* FILL IN HERE *) Admitted.
Lemma ev_even_firsttry : ∀ n,
ev n → ∃ k, n = double k.
Proof.
(* WORKED IN CLASS *)
We could try to proceed by case analysis or induction on n. But
since ev is mentioned in a premise, this strategy would probably
lead to a dead end, as in the previous section. Thus, it seems
better to first try inversion on the evidence for ev. Indeed,
the first case can be solved trivially.
intros n E. inversion E as [| n' E'].
- (* E = ev_0 *)
∃ 0. reflexivity.
- (* E = ev_SS n' E' *) simpl.
Unfortunately, the second case is harder. We need to show ∃
k, S (S n') = double k, but the only available assumption is
E', which states that ev n' holds. Since this isn't directly
useful, it seems that we are stuck and that performing case
analysis on E was a waste of time.
If we look more closely at our second goal, however, we can see
that something interesting happened: By performing case analysis
on E, we were able to reduce the original result to an similar
one that involves a different piece of evidence for ev: E'.
More formally, we can finish our proof by showing that
∃ k', n' = double k',
which is the same as the original statement, but with n' instead
of n. Indeed, it is not difficult to convince Coq that this
intermediate result suffices.
assert (I : (∃ k', n' = double k') →
(∃ k, S (S n') = double k)).
{ intros [k' Hk']. rewrite Hk'. ∃ (S k'). reflexivity. }
apply I. (* reduce the original goal to the new one *)
Admitted.
Induction on Evidence
Lemma ev_even : ∀ n,
ev n → ∃ k, n = double k.
Proof.
intros n E.
induction E as [|n' E' IH].
- (* E = ev_0 *)
∃ 0. reflexivity.
- (* E = ev_SS n' E'
with IH : exists k', n' = double k' *)
destruct IH as [k' Hk'].
rewrite Hk'. ∃ (S k'). reflexivity.
Qed.
Here, we can see that Coq produced an IH that corresponds to
E', the single recursive occurrence of ev in its own
definition. Since E' mentions n', the induction hypothesis
talks about n', as opposed to n or some other number.
The equivalence between the second and third definitions of
evenness now follows.
Theorem ev_even_iff : ∀ n,
ev n ↔ ∃ k, n = double k.
Proof.
intros n. split.
- (* -> *) apply ev_even.
- (* <- *) intros [k Hk]. rewrite Hk. apply ev_double.
Qed.
As we will see in later chapters, induction on evidence is a
recurring technique across many areas, and in particular when
formalizing the semantics of programming languages, where many
properties of interest are defined inductively.
The following exercises provide simple examples of this
technique, to help you familiarize yourself with it.
Exercise: 2 stars (ev_sum)
Theorem ev_sum : ∀ n m, ev n → ev m → ev (n + m).
Proof.
(* FILL IN HERE *) Admitted.
☐
Proof.
(* FILL IN HERE *) Admitted.
Exercise: 4 stars, advanced, optional (ev_alternate)
In general, there may be multiple ways of defining a property inductively. For example, here's a (slightly contrived) alternative definition for ev:Inductive ev' : nat → Prop :=
| ev'_0 : ev' 0
| ev'_2 : ev' 2
| ev'_sum : ∀ n m, ev' n → ev' m → ev' (n + m).
Prove that this definition is logically equivalent to the old
one. (You may want to look at the previous theorem when you get
to the induction step.)
Theorem ev'_ev : ∀ n, ev' n ↔ ev n.
Proof.
(* FILL IN HERE *) Admitted.
Exercise: 3 stars, advanced, recommended (ev_ev__ev)
Finding the appropriate thing to do induction on is a bit tricky here:Theorem ev_ev__ev : ∀ n m,
ev (n+m) → ev n → ev m.
Proof.
(* FILL IN HERE *) Admitted.
Exercise: 3 stars, optional (ev_plus_plus)
This exercise just requires applying existing lemmas. No induction or even case analysis is needed, though some of the rewriting may be tedious.Theorem ev_plus_plus : ∀ n m p,
ev (n+m) → ev (n+p) → ev (m+p).
Proof.
(* FILL IN HERE *) Admitted.
Inductive Relations
Module Playground.
One useful example is the "less than or equal to" relation on
numbers.
The following definition should be fairly intuitive. It
says that there are two ways to give evidence that one number is
less than or equal to another: either observe that they are the
same number, or give evidence that the first is less than or equal
to the predecessor of the second.
Inductive le : nat → nat → Prop :=
| le_n : ∀ n, le n n
| le_S : ∀ n m, (le n m) → (le n (S m)).
Notation "m ≤ n" := (le m n).
Proofs of facts about ≤ using the constructors le_n and
le_S follow the same patterns as proofs about properties, like
ev above. We can apply the constructors to prove ≤
goals (e.g., to show that 3≤3 or 3≤6), and we can use
tactics like inversion to extract information from ≤
hypotheses in the context (e.g., to prove that (2 ≤ 1) →
2+2=5.)
Here are some sanity checks on the definition. (Notice that,
although these are the same kind of simple "unit tests" as we gave
for the testing functions we wrote in the first few lectures, we
must construct their proofs explicitly — simpl and
reflexivity don't do the job, because the proofs aren't just a
matter of simplifying computations.)
Theorem test_le1 :
3 ≤ 3.
Proof.
(* WORKED IN CLASS *)
apply le_n. Qed.
Theorem test_le2 :
3 ≤ 6.
Proof.
(* WORKED IN CLASS *)
apply le_S. apply le_S. apply le_S. apply le_n. Qed.
Theorem test_le3 :
(2 ≤ 1) → 2 + 2 = 5.
Proof.
(* WORKED IN CLASS *)
intros H. inversion H. inversion H2. Qed.
The "strictly less than" relation n < m can now be defined
in terms of le.
End Playground.
Definition lt (n m:nat) := le (S n) m.
Notation "m < n" := (lt m n).
Here are a few more simple relations on numbers:
Inductive square_of : nat → nat → Prop :=
| sq : ∀ n:nat, square_of n (n * n).
Inductive next_nat : nat → nat → Prop :=
| nn : ∀ n:nat, next_nat n (S n).
Inductive next_even : nat → nat → Prop :=
| ne_1 : ∀ n, ev (S n) → next_even n (S n)
| ne_2 : ∀ n, ev (S (S n)) → next_even n (S (S n)).
Exercise: 2 stars, optional (total_relation)
Define an inductive binary relation total_relation that holds between every pair of natural numbers.(* FILL IN HERE *)
Exercise: 2 stars, optional (empty_relation)
Define an inductive binary relation empty_relation (on numbers) that never holds.(* FILL IN HERE *)
Exercise: 3 stars, optional (le_exercises)
Here are a number of facts about the ≤ and < relations that we are going to need later in the course. The proofs make good practice exercises.Lemma le_trans : ∀ m n o, m ≤ n → n ≤ o → m ≤ o.
Proof.
(* FILL IN HERE *) Admitted.
Theorem O_le_n : ∀ n,
0 ≤ n.
Proof.
(* FILL IN HERE *) Admitted.
Theorem n_le_m__Sn_le_Sm : ∀ n m,
n ≤ m → S n ≤ S m.
Proof.
(* FILL IN HERE *) Admitted.
Theorem Sn_le_Sm__n_le_m : ∀ n m,
S n ≤ S m → n ≤ m.
Proof.
(* FILL IN HERE *) Admitted.
Theorem le_plus_l : ∀ a b,
a ≤ a + b.
Proof.
(* FILL IN HERE *) Admitted.
Theorem plus_lt : ∀ n1 n2 m,
n1 + n2 < m →
n1 < m ∧ n2 < m.
Proof.
unfold lt.
(* FILL IN HERE *) Admitted.
Theorem lt_S : ∀ n m,
n < m →
n < S m.
Proof.
(* FILL IN HERE *) Admitted.
Theorem leb_complete : ∀ n m,
leb n m = true → n ≤ m.
Proof.
(* FILL IN HERE *) Admitted.
Hint: The next one may be easiest to prove by induction on m.
Theorem leb_correct : ∀ n m,
n ≤ m →
leb n m = true.
Proof.
(* FILL IN HERE *) Admitted.
Hint: This theorem can easily be proved without using induction.
Theorem leb_true_trans : ∀ n m o,
leb n m = true → leb m o = true → leb n o = true.
Proof.
(* FILL IN HERE *) Admitted.
Theorem leb_iff : ∀ n m,
leb n m = true ↔ n ≤ m.
Proof.
(* FILL IN HERE *) Admitted.
☐
leb n m = true ↔ n ≤ m.
Proof.
(* FILL IN HERE *) Admitted.
Module R.
Exercise: 3 stars, recommendedM (R_provability)
We can define three-place relations, four-place relations, etc., in just the same way as binary relations. For example, consider the following three-place relation on numbers:Inductive R : nat → nat → nat → Prop :=
| c1 : R 0 0 0
| c2 : ∀ m n o, R m n o → R (S m) n (S o)
| c3 : ∀ m n o, R m n o → R m (S n) (S o)
| c4 : ∀ m n o, R (S m) (S n) (S (S o)) → R m n o
| c5 : ∀ m n o, R m n o → R n m o.
- Which of the following propositions are provable?
- R 1 1 2
- R 2 2 6
- If we dropped constructor c5 from the definition of R,
would the set of provable propositions change? Briefly (1
sentence) explain your answer.
- If we dropped constructor c4 from the definition of R, would the set of provable propositions change? Briefly (1 sentence) explain your answer.
☐
Exercise: 3 stars, optional (R_fact)
The relation R above actually encodes a familiar function. Figure out which function; then state and prove this equivalence in Coq?Definition fR : nat → nat → nat
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Theorem R_equiv_fR : ∀ m n o, R m n o ↔ fR m n = o.
Proof.
(* FILL IN HERE *) Admitted.
End R.
Exercise: 4 stars, advanced (subsequence)
A list is a subsequence of another list if all of the elements in the first list occur in the same order in the second list, possibly with some extra elements in between. For example,
[1;2;3]
is a subsequence of each of the lists
[1;2;3]
[1;1;1;2;2;3]
[1;2;7;3]
[5;6;1;9;9;2;7;3;8]
but it is not a subsequence of any of the lists
[1;1;1;2;2;3]
[1;2;7;3]
[5;6;1;9;9;2;7;3;8]
[1;2]
[1;3]
[5;6;2;1;7;3;8].
[1;3]
[5;6;2;1;7;3;8].
- Define an inductive proposition subseq on list nat that
captures what it means to be a subsequence. (Hint: You'll need
three cases.)
- Prove subseq_refl that subsequence is reflexive, that is,
any list is a subsequence of itself.
- Prove subseq_app that for any lists l1, l2, and l3,
if l1 is a subsequence of l2, then l1 is also a subsequence
of l2 ++ l3.
- (Optional, harder) Prove subseq_trans that subsequence is transitive — that is, if l1 is a subsequence of l2 and l2 is a subsequence of l3, then l1 is a subsequence of l3. Hint: choose your induction carefully!
(* FILL IN HERE *)
Exercise: 2 stars, optionalM (R_provability2)
Suppose we give Coq the following definition:
Inductive R : nat → list nat → Prop :=
| c1 : R 0 []
| c2 : ∀ n l, R n l → R (S n) (n :: l)
| c3 : ∀ n l, R (S n) l → R n l.
Which of the following propositions are provable?
| c1 : R 0 []
| c2 : ∀ n l, R n l → R (S n) (n :: l)
| c3 : ∀ n l, R (S n) l → R n l.
- R 2 [1;0]
- R 1 [1;2;1;0]
- R 6 [3;2;1;0]
Case Study: Regular Expressions
Inductive reg_exp {T : Type} : Type :=
| EmptySet : reg_exp
| EmptyStr : reg_exp
| Char : T → reg_exp
| App : reg_exp → reg_exp → reg_exp
| Union : reg_exp → reg_exp → reg_exp
| Star : reg_exp → reg_exp.
Note that this definition is polymorphic: Regular
expressions in reg_exp T describe strings with characters drawn
from T — that is, lists of elements of T.
(We depart slightly from standard practice in that we do not
require the type T to be finite. This results in a somewhat
different theory of regular expressions, but the difference is not
significant for our purposes.)
We connect regular expressions and strings via the following
rules, which define when a regular expression matches some
string:
We can easily translate this informal definition into an
Inductive one as follows:
- The expression EmptySet does not match any string.
- The expression EmptyStr matches the empty string [].
- The expression Char x matches the one-character string [x].
- If re1 matches s1, and re2 matches s2, then App re1
re2 matches s1 ++ s2.
- If at least one of re1 and re2 matches s, then Union re1
re2 matches s.
- Finally, if we can write some string s as the concatenation of
a sequence of strings s = s_1 ++ ... ++ s_k, and the
expression re matches each one of the strings s_i, then
Star re matches s.
As a special case, the sequence of strings may be empty, so Star re always matches the empty string [] no matter what re is.
Inductive exp_match {T} : list T → reg_exp → Prop :=
| MEmpty : exp_match [] EmptyStr
| MChar : ∀ x, exp_match [x] (Char x)
| MApp : ∀ s1 re1 s2 re2,
exp_match s1 re1 →
exp_match s2 re2 →
exp_match (s1 ++ s2) (App re1 re2)
| MUnionL : ∀ s1 re1 re2,
exp_match s1 re1 →
exp_match s1 (Union re1 re2)
| MUnionR : ∀ re1 s2 re2,
exp_match s2 re2 →
exp_match s2 (Union re1 re2)
| MStar0 : ∀ re, exp_match [] (Star re)
| MStarApp : ∀ s1 s2 re,
exp_match s1 re →
exp_match s2 (Star re) →
exp_match (s1 ++ s2) (Star re).
Again, for readability, we can also display this definition using
inference-rule notation. At the same time, let's introduce a more
readable infix notation.
Notation "s =~ re" := (exp_match s re) (at level 80).
| (MEmpty) | |
| [] =~ EmptyStr |
| (MChar) | |
| [x] =~ Char x |
| s1 =~ re1 s2 =~ re2 | (MApp) |
| s1 ++ s2 =~ App re1 re2 |
| s1 =~ re1 | (MUnionL) |
| s1 =~ Union re1 re2 |
| s2 =~ re2 | (MUnionR) |
| s2 =~ Union re1 re2 |
| (MStar0) | |
| [] =~ Star re |
| s1 =~ re s2 =~ Star re | (MStarApp) |
| s1 ++ s2 =~ Star re |
Example reg_exp_ex1 : [1] =~ Char 1.
Proof.
apply MChar.
Qed.
Example reg_exp_ex2 : [1; 2] =~ App (Char 1) (Char 2).
Proof.
apply (MApp [1] _ [2]).
- apply MChar.
- apply MChar.
Qed.
(Notice how the last example applies MApp to the strings [1]
and [2] directly. Since the goal mentions [1; 2] instead of
[1] ++ [2], Coq wouldn't be able to figure out how to split the
string on its own.)
Using inversion, we can also show that certain strings do not
match a regular expression:
Example reg_exp_ex3 : ¬ ([1; 2] =~ Char 1).
Proof.
intros H. inversion H.
Qed.
We can define helper functions to help write down regular
expressions. The reg_exp_of_list function constructs a regular
expression that matches exactly the list that it receives as an
argument:
Fixpoint reg_exp_of_list {T} (l : list T) :=
match l with
| [] ⇒ EmptyStr
| x :: l' ⇒ App (Char x) (reg_exp_of_list l')
end.
Example reg_exp_ex4 : [1; 2; 3] =~ reg_exp_of_list [1; 2; 3].
Proof.
simpl. apply (MApp [1]).
{ apply MChar. }
apply (MApp [2]).
{ apply MChar. }
apply (MApp [3]).
{ apply MChar. }
apply MEmpty.
Qed.
We can also prove general facts about exp_match. For instance,
the following lemma shows that every string s that matches re
also matches Star re.
Lemma MStar1 :
∀ T s (re : @reg_exp T) ,
s =~ re →
s =~ Star re.
Proof.
intros T s re H.
rewrite <- (app_nil_r _ s).
apply (MStarApp s [] re).
- apply H.
- apply MStar0.
Qed.
(Note the use of app_nil_r to change the goal of the theorem to
exactly the same shape expected by MStarApp.)
Exercise: 3 stars (exp_match_ex1)
The following lemmas show that the informal matching rules given at the beginning of the chapter can be obtained from the formal inductive definition.Lemma empty_is_empty : ∀ T (s : list T),
¬ (s =~ EmptySet).
Proof.
(* FILL IN HERE *) Admitted.
Lemma MUnion' : ∀ T (s : list T) (re1 re2 : @reg_exp T),
s =~ re1 ∨ s =~ re2 →
s =~ Union re1 re2.
Proof.
(* FILL IN HERE *) Admitted.
The next lemma is stated in terms of the fold function from the
Poly chapter: If ss : list (list T) represents a sequence of
strings s1, ..., sn, then fold app ss [] is the result of
concatenating them all together.
Lemma MStar' : ∀ T (ss : list (list T)) (re : reg_exp),
(∀ s, In s ss → s =~ re) →
fold app ss [] =~ Star re.
Proof.
(* FILL IN HERE *) Admitted.
Exercise: 4 stars (reg_exp_of_list)
Prove that reg_exp_of_list satisfies the following specification:Lemma reg_exp_of_list_spec : ∀ T (s1 s2 : list T),
s1 =~ reg_exp_of_list s2 ↔ s1 = s2.
Proof.
(* FILL IN HERE *) Admitted.
Fixpoint re_chars {T} (re : reg_exp) : list T :=
match re with
| EmptySet ⇒ []
| EmptyStr ⇒ []
| Char x ⇒ [x]
| App re1 re2 ⇒ re_chars re1 ++ re_chars re2
| Union re1 re2 ⇒ re_chars re1 ++ re_chars re2
| Star re ⇒ re_chars re
end.
We can then phrase our theorem as follows:
Theorem in_re_match : ∀ T (s : list T) (re : reg_exp) (x : T),
s =~ re →
In x s →
In x (re_chars re).
Proof.
intros T s re x Hmatch Hin.
induction Hmatch
as [
|x'
|s1 re1 s2 re2 Hmatch1 IH1 Hmatch2 IH2
|s1 re1 re2 Hmatch IH|re1 s2 re2 Hmatch IH
|re|s1 s2 re Hmatch1 IH1 Hmatch2 IH2].
(* WORKED IN CLASS *)
- (* MEmpty *)
apply Hin.
- (* MChar *)
apply Hin.
- simpl. rewrite in_app_iff in *.
destruct Hin as [Hin | Hin].
+ (* In x s1 *)
left. apply (IH1 Hin).
+ (* In x s2 *)
right. apply (IH2 Hin).
- (* MUnionL *)
simpl. rewrite in_app_iff.
left. apply (IH Hin).
- (* MUnionR *)
simpl. rewrite in_app_iff.
right. apply (IH Hin).
- (* MStar0 *)
destruct Hin.
Something interesting happens in the MStarApp case. We obtain
two induction hypotheses: One that applies when x occurs in
s1 (which matches re), and a second one that applies when x
occurs in s2 (which matches Star re). This is a good
illustration of why we need induction on evidence for exp_match,
as opposed to re: The latter would only provide an induction
hypothesis for strings that match re, which would not allow us
to reason about the case In x s2.
- (* MStarApp *)
simpl. rewrite in_app_iff in Hin.
destruct Hin as [Hin | Hin].
+ (* In x s1 *)
apply (IH1 Hin).
+ (* In x s2 *)
apply (IH2 Hin).
Qed.
Exercise: 4 stars (re_not_empty)
Write a recursive function re_not_empty that tests whether a regular expression matches some string. Prove that your function is correct.Fixpoint re_not_empty {T : Type} (re : @reg_exp T) : bool
(* REPLACE THIS LINE WITH ":= _your_definition_ ." *). Admitted.
Lemma re_not_empty_correct : ∀ T (re : @reg_exp T),
(∃ s, s =~ re) ↔ re_not_empty re = true.
Proof.
(* FILL IN HERE *) Admitted.
The remember Tactic
Lemma star_app: ∀ T (s1 s2 : list T) (re : @reg_exp T),
s1 =~ Star re →
s2 =~ Star re →
s1 ++ s2 =~ Star re.
Proof.
intros T s1 s2 re H1.
Just doing an inversion on H1 won't get us very far in the
recursive cases. (Try it!). So we need induction. Here is a naive
first attempt:
induction H1
as [|x'|s1 re1 s2' re2 Hmatch1 IH1 Hmatch2 IH2
|s1 re1 re2 Hmatch IH|re1 s2' re2 Hmatch IH
|re''|s1 s2' re'' Hmatch1 IH1 Hmatch2 IH2].
But now, although we get seven cases (as we would expect from the
definition of exp_match), we have lost a very important bit of
information from H1: the fact that s1 matched something of the
form Star re. This means that we have to give proofs for all
seven constructors of this definition, even though all but two of
them (MStar0 and MStarApp) are contradictory. We can still
get the proof to go through for a few constructors, such as
MEmpty...
- (* MEmpty *)
simpl. intros H. apply H.
... but most cases get stuck. For MChar, for instance, we
must show that
s2 =~ Char x' → x' :: s2 =~ Char x',
which is clearly impossible.
- (* MChar. Stuck... *)
Abort.
The problem is that induction over a Prop hypothesis only works
properly with hypotheses that are completely general, i.e., ones
in which all the arguments are variables, as opposed to more
complex expressions, such as Star re.
(In this respect, induction on evidence behaves more like
destruct than like inversion.)
We can solve this problem by generalizing over the problematic
expressions with an explicit equality:
Lemma star_app: ∀ T (s1 s2 : list T) (re re' : reg_exp),
re' = Star re →
s1 =~ re' →
s2 =~ Star re →
s1 ++ s2 =~ Star re.
We can now proceed by performing induction over evidence directly,
because the argument to the first hypothesis is sufficiently
general, which means that we can discharge most cases by inverting
the re' = Star re equality in the context.
This idiom is so common that Coq provides a tactic to
automatically generate such equations for us, avoiding thus the
need for changing the statements of our theorems.
Abort.
Invoking the tactic remember e as x causes Coq to (1) replace
all occurrences of the expression e by the variable x, and (2)
add an equation x = e to the context. Here's how we can use it
to show the above result:
Lemma star_app: ∀ T (s1 s2 : list T) (re : reg_exp),
s1 =~ Star re →
s2 =~ Star re →
s1 ++ s2 =~ Star re.
Proof.
intros T s1 s2 re H1.
remember (Star re) as re'.
We now have Heqre' : re' = Star re.
generalize dependent s2.
induction H1
as [|x'|s1 re1 s2' re2 Hmatch1 IH1 Hmatch2 IH2
|s1 re1 re2 Hmatch IH|re1 s2' re2 Hmatch IH
|re''|s1 s2' re'' Hmatch1 IH1 Hmatch2 IH2].
The Heqre' is contradictory in most cases, which allows us to
conclude immediately.
- (* MEmpty *) inversion Heqre'.
- (* MChar *) inversion Heqre'.
- (* MApp *) inversion Heqre'.
- (* MUnionL *) inversion Heqre'.
- (* MUnionR *) inversion Heqre'.
The interesting cases are those that correspond to Star. Note
that the induction hypothesis IH2 on the MStarApp case
mentions an additional premise Star re'' = Star re', which
results from the equality generated by remember.
- (* MStar0 *)
inversion Heqre'. intros s H. apply H.
- (* MStarApp *)
inversion Heqre'. rewrite H0 in IH2, Hmatch1.
intros s2 H1. rewrite <- app_assoc.
apply MStarApp.
+ apply Hmatch1.
+ apply IH2.
* reflexivity.
* apply H1.
Qed.
Exercise: 4 stars (exp_match_ex2)
Lemma MStar'' : ∀ T (s : list T) (re : reg_exp),
s =~ Star re →
∃ ss : list (list T),
s = fold app ss []
∧ ∀ s', In s' ss → s' =~ re.
Proof.
(* FILL IN HERE *) Admitted.
Exercise: 5 stars, advanced (pumping)
One of the first really interesting theorems in the theory of regular expressions is the so-called pumping lemma, which states, informally, that any sufficiently long string s matching a regular expression re can be "pumped" by repeating some middle section of s an arbitrary number of times to produce a new string also matching re.Module Pumping.
Fixpoint pumping_constant {T} (re : @reg_exp T) : nat :=
match re with
| EmptySet ⇒ 0
| EmptyStr ⇒ 1
| Char _ ⇒ 2
| App re1 re2 ⇒
pumping_constant re1 + pumping_constant re2
| Union re1 re2 ⇒
pumping_constant re1 + pumping_constant re2
| Star _ ⇒ 1
end.
Next, it is useful to define an auxiliary function that repeats a
string (appends it to itself) some number of times.
Fixpoint napp {T} (n : nat) (l : list T) : list T :=
match n with
| 0 ⇒ []
| S n' ⇒ l ++ napp n' l
end.
Lemma napp_plus: ∀ T (n m : nat) (l : list T),
napp (n + m) l = napp n l ++ napp m l.
Proof.
intros T n m l.
induction n as [|n IHn].
- reflexivity.
- simpl. rewrite IHn, app_assoc. reflexivity.
Qed.
Now, the pumping lemma itself says that, if s =~ re and if the
length of s is at least the pumping constant of re, then s
can be split into three substrings s1 ++ s2 ++ s3 in such a way
that s2 can be repeated any number of times and the result, when
combined with s1 and s3 will still match re. Since s2 is
also guaranteed not to be the empty string, this gives us
a (constructive!) way to generate strings matching re that are
as long as we like.
Lemma pumping : ∀ T (re : @reg_exp T) s,
s =~ re →
pumping_constant re ≤ length s →
∃ s1 s2 s3,
s = s1 ++ s2 ++ s3 ∧
s2 ≠ [] ∧
∀ m, s1 ++ napp m s2 ++ s3 =~ re.
To streamline the proof (which you are to fill in), the omega
tactic, which is enabled by the following Require, is helpful in
several places for automatically completing tedious low-level
arguments involving equalities or inequalities over natural
numbers. We'll return to omega in a later chapter, but feel
free to experiment with it now if you like. The first case of the
induction gives an example of how it is used.
Import Coq.omega.Omega.
Proof.
intros T re s Hmatch.
induction Hmatch
as [ | x | s1 re1 s2 re2 Hmatch1 IH1 Hmatch2 IH2
| s1 re1 re2 Hmatch IH | re1 s2 re2 Hmatch IH
| re | s1 s2 re Hmatch1 IH1 Hmatch2 IH2 ].
- (* MEmpty *)
simpl. omega.
(* FILL IN HERE *) Admitted.
End Pumping.
Case Study: Improving Reflection
Theorem filter_not_empty_In : ∀ n l,
filter (beq_nat n) l ≠ [] →
In n l.
Proof.
intros n l. induction l as [|m l' IHl'].
- (* l = *)
simpl. intros H. apply H. reflexivity.
- (* l = m :: l' *)
simpl. destruct (beq_nat n m) eqn:H.
+ (* beq_nat n m = true *)
intros _. rewrite beq_nat_true_iff in H. rewrite H.
left. reflexivity.
+ (* beq_nat n m = false *)
intros H'. right. apply IHl'. apply H'.
Qed.
In the first branch after destruct, we explicitly apply
the beq_nat_true_iff lemma to the equation generated by
destructing beq_nat n m, to convert the assumption beq_nat n m
= true into the assumption n = m; then we had to rewrite
using this assumption to complete the case.
We can streamline this by defining an inductive proposition that
yields a better case-analysis principle for beq_nat n m.
Instead of generating an equation such as beq_nat n m = true,
which is generally not directly useful, this principle gives us
right away the assumption we really need: n = m.
We'll actually define something a bit more general, which can be
used with arbitrary properties (and not just equalities):
Module FirstTry.
Inductive reflect : Prop → bool → Prop :=
| ReflectT : ∀ (P:Prop), P → reflect P true
| ReflectF : ∀ (P:Prop), ¬ P → reflect P false.
End FirstTry.
Before explaining this, let's rearrange it a little: Since the
types of both ReflectT and ReflectF begin with
∀ (P:Prop), we can make the definition a bit more readable
and easier to work with by making P a parameter of the whole
Inductive declaration.
Inductive reflect (P : Prop) : bool → Prop :=
| ReflectT : P → reflect P true
| ReflectF : ¬ P → reflect P false.
The reflect property takes two arguments: a proposition
P and a boolean b. Intuitively, it states that the property
P is reflected in (i.e., equivalent to) the boolean b: that
is, P holds if and only if b = true. To see this, notice
that, by definition, the only way we can produce evidence that
reflect P true holds is by showing that P is true and using
the ReflectT constructor. If we invert this statement, this
means that it should be possible to extract evidence for P from
a proof of reflect P true. Conversely, the only way to show
reflect P false is by combining evidence for ¬ P with the
ReflectF constructor.
It is easy to formalize this intuition and show that the two
statements are indeed equivalent:
Theorem iff_reflect : ∀ P b, (P ↔ b = true) → reflect P b.
Proof.
(* WORKED IN CLASS *)
intros P b H. destruct b.
- apply ReflectT. rewrite H. reflexivity.
- apply ReflectF. rewrite H. intros H'. inversion H'.
Qed.
Theorem reflect_iff : ∀ P b, reflect P b → (P ↔ b = true).
Proof.
(* FILL IN HERE *) Admitted.
☐
Proof.
(* FILL IN HERE *) Admitted.
Lemma beq_natP : ∀ n m, reflect (n = m) (beq_nat n m).
Proof.
intros n m. apply iff_reflect. rewrite beq_nat_true_iff. reflexivity.
Qed.
The new proof of filter_not_empty_In now goes as follows.
Notice how the calls to destruct and apply are combined into a
single call to destruct.
(To see this clearly, look at the two proofs of
filter_not_empty_In with Coq and observe the differences in
proof state at the beginning of the first case of the
destruct.)
Theorem filter_not_empty_In' : ∀ n l,
filter (beq_nat n) l ≠ [] →
In n l.
Proof.
intros n l. induction l as [|m l' IHl'].
- (* l = *)
simpl. intros H. apply H. reflexivity.
- (* l = m :: l' *)
simpl. destruct (beq_natP n m) as [H | H].
+ (* n = m *)
intros _. rewrite H. left. reflexivity.
+ (* n <> m *)
intros H'. right. apply IHl'. apply H'.
Qed.
Fixpoint count n l :=
match l with
| [] ⇒ 0
| m :: l' ⇒ (if beq_nat n m then 1 else 0) + count n l'
end.
Theorem beq_natP_practice : ∀ n l,
count n l = 0 → ~(In n l).
Proof.
(* FILL IN HERE *) Admitted.
Additional Exercises
Exercise: 3 stars, recommended (nostutter)
Formulating inductive definitions of properties is an important skill you'll need in this course. Try to solve this exercise without any help at all.Inductive nostutter {X:Type} : list X → Prop :=
(* FILL IN HERE *)
.
Make sure each of these tests succeeds, but feel free to change
the suggested proof (in comments) if the given one doesn't work
for you. Your definition might be different from ours and still
be correct, in which case the examples might need a different
proof. (You'll notice that the suggested proofs use a number of
tactics we haven't talked about, to make them more robust to
different possible ways of defining nostutter. You can probably
just uncomment and use them as-is, but you can also prove each
example with more basic tactics.)
Example test_nostutter_1: nostutter [3;1;4;1;5;6].
(* FILL IN HERE *) Admitted.
(*
Proof. repeat constructor; apply beq_nat_false_iff; auto.
Qed.
*)
Example test_nostutter_2: nostutter (@nil nat).
(* FILL IN HERE *) Admitted.
(*
Proof. repeat constructor; apply beq_nat_false_iff; auto.
Qed.
*)
Example test_nostutter_3: nostutter [5].
(* FILL IN HERE *) Admitted.
(*
Proof. repeat constructor; apply beq_nat_false; auto. Qed.
*)
Example test_nostutter_4: not (nostutter [3;1;1;4]).
(* FILL IN HERE *) Admitted.
(*
Proof. intro.
repeat match goal with
h: nostutter _ |- _ => inversion h; clear h; subst
end.
contradiction H1; auto. Qed.
*)
Exercise: 4 stars, advanced (filter_challenge)
Let's prove that our definition of filter from the Poly chapter matches an abstract specification. Here is the specification, written out informally in English:
[1;4;6;2;3]
is an in-order merge of
[1;6;2]
and
[4;3].
Now, suppose we have a set X, a function test: X→bool, and a
list l of type list X. Suppose further that l is an
in-order merge of two lists, l1 and l2, such that every item
in l1 satisfies test and no item in l2 satisfies test. Then
filter test l = l1.
(* FILL IN HERE *)
Exercise: 5 stars, advanced, optional (filter_challenge_2)
A different way to characterize the behavior of filter goes like this: Among all subsequences of l with the property that test evaluates to true on all their members, filter test l is the longest. Formalize this claim and prove it.(* FILL IN HERE *)
Exercise: 4 stars, optional (palindromes)
A palindrome is a sequence that reads the same backwards as forwards.- Define an inductive proposition pal on list X that
captures what it means to be a palindrome. (Hint: You'll need
three cases. Your definition should be based on the structure
of the list; just having a single constructor like
c : ∀ l, l = rev l → pal lmay seem obvious, but will not work very well.)
- Prove (pal_app_rev) that
∀ l, pal (l ++ rev l).
- Prove (pal_rev that)
∀ l, pal l → l = rev l.
(* FILL IN HERE *)
Exercise: 5 stars, optional (palindrome_converse)
Again, the converse direction is significantly more difficult, due to the lack of evidence. Using your definition of pal from the previous exercise, prove that
∀ l, l = rev l → pal l.
(* FILL IN HERE *)
Exercise: 4 stars, advanced, optional (NoDup)
Recall the definition of the In property from the Logic chapter, which asserts that a value x appears at least once in a list l:(* Fixpoint In (A : Type) (x : A) (l : list A) : Prop :=
match l with
| => False
| x' :: l' => x' = x \/ In A x l'
end *)
Your first task is to use In to define a proposition disjoint X
l1 l2, which should be provable exactly when l1 and l2 are
lists (with elements of type X) that have no elements in
common.
(* FILL IN HERE *)
Next, use In to define an inductive proposition NoDup X
l, which should be provable exactly when l is a list (with
elements of type X) where every member is different from every
other. For example, NoDup nat [1;2;3;4] and NoDup
bool [] should be provable, while NoDup nat [1;2;1] and
NoDup bool [true;true] should not be.
(* FILL IN HERE *)
Finally, state and prove one or more interesting theorems relating
disjoint, NoDup and ++ (list append).
(* FILL IN HERE *)
Exercise: 4 stars, advanced, optional (pigeonhole principle)
The pigeonhole principle states a basic fact about counting: if we distribute more than n items into n pigeonholes, some pigeonhole must contain at least two items. As often happens, this apparently trivial fact about numbers requires non-trivial machinery to prove, but we now have enough...Lemma in_split : ∀ (X:Type) (x:X) (l:list X),
In x l →
∃ l1 l2, l = l1 ++ x :: l2.
Proof.
(* FILL IN HERE *) Admitted.
Now define a property repeats such that repeats X l asserts
that l contains at least one repeated element (of type X).
Inductive repeats {X:Type} : list X → Prop :=
(* FILL IN HERE *)
.
Now, here's a way to formalize the pigeonhole principle. Suppose
list l2 represents a list of pigeonhole labels, and list l1
represents the labels assigned to a list of items. If there are
more items than labels, at least two items must have the same
label — i.e., list l1 must contain repeats.
This proof is much easier if you use the excluded_middle
hypothesis to show that In is decidable, i.e., ∀ x l, (In x
l) ∨ ¬ (In x l). However, it is also possible to make the proof
go through without assuming that In is decidable; if you
manage to do this, you will not need the excluded_middle
hypothesis.
Theorem pigeonhole_principle: ∀ (X:Type) (l1 l2:list X),
excluded_middle →
(∀ x, In x l1 → In x l2) →
length l2 < length l1 →
repeats l1.
Proof.
intros X l1. induction l1 as [|x l1' IHl1'].
(* FILL IN HERE *) Admitted.


Migrating from MySQL to PostgreSQLby Zach Beane |
Know SQL. If your only experience with SQL is through MySQL, many things in PostgreSQL (and indeed, any other database system) will seem alien and strange. The idioms you may have developed to work with MySQL may not be the ideal approach when using PostgreSQL. In particular, you have a set of new tools (views, triggers, stored procedures, consistency checks, and more) that you should try to take advantage of.
Get a good book on SQL. The Practical SQL Handbook is pretty handy. Joe Celko's SQL for Smarties, despite the silly title, is a down-to-earth, nuts-and-bolts practical book about using SQL to its fullest. The free online book SQL for Web Nerds, though Oracle-specific, will give you ideas for good idioms.
So far I've written a Perl script that converts the data model pretty well. It handles enums (it converts them to varchars with check constraints on the possible values) and auto_increment fields. It also converts MySQL's integer and time types to compatible PostgreSQL types.
The script outputs SQL statements that seem to work with CVS PostgreSQL. The CVS version will eventually become PostgreSQL 7.1.
| MySQL | PostgreSQL |
|---|---|
create table foo ( id int not null auto_increment primary key, state enum('enabled', 'disabled') ); foo's data |
create table foo ( id int not null primary key default nextval('foo_id_seq'), state varchar(8) check (state in ('enabled', 'disabled')) ); foo's data create sequence foo_id_seq; select setval('foo_id_seq', (select max(id) from foo)); |
To be handled:
Joseph Speigle wrote to me about an actively-maintained (as of July, 2004) mysql2pgsql Perl script.
MySQL has some interesting functions that are either unavailable in PostgreSQL, or supported by functions of slightly different syntax. For example, ifnull() in MySQL is similar to coalesce() in PostgreSQL.
To ease the transition from the MySQL that's embedded in all my pages, I've created a set of SQL functions that recreate the MySQL functions.
Converted:
update Christopher Kings-Lynn wrote to tell me about a more thorough project to implement MySQL functions in PostgreSQL. You can find it here.
This list isn't an endorsement of MySQL; these examples mainly come up because MySQL is much less conformant with SQL standards in general.
select name, count(*) as score from mytable group by name having score > 10
For PostgreSQL, you have to write out the expression again:
select name, count(*) as score from mytable group by name having count(*) > 10
It doesn't mind having aliases in ORDER BY, but you can't use it in HAVING. Tom Lane explains.
NAMEDATALEN is defined in src/include/postgres_ext.h. The name length is NAMEDATALEN - 1.


Home
About
Club History
Schedule
Contact
Gallery
Sponsors
Close
Polo
Store
Facebook
Upcoming
Benefits
Menu
Polo Caption
Polo Caption
Polo Caption
Horse
Previous
Next
Play/Pause
Your browser does not support HTML5 video.


| Harrowing story of a young Jewish girl who, with her family and their friends is forced into hiding in an attic in Nazi-occupied Amsterdam. | |
| Genres: | Biography, Drama, Family, History, War |
| Director: | George Stevens |
| Writer: | Frances Goodrich, Albert Hackett, Anne Frank, George Stevens |
Cast: | Anne Frank - Millie Perkins Otto Frank - Joseph Schildkraut Mrs. Petronella Van Daan - Shelley Winters Peter Van Daan - Richard Beymer Mrs. Edith Frank - Gusti Huber Mr. Hans Van Daan - Lou Jacobi Margot Frank - Diane Baker Kraler - Douglas Spencer Miep - Dodie Heath Mr. Albert Dussell - Ed Wynn Dutch Workman - Arthur Berkeley SS Man - Robert Boon Dutch Workman - John Corrydon SS Man - Delmar Erickson Sanne Devries - Gretchen Goertz Workman in Shop - William Kirschner British Radio Announcer - Edmund Purdom Night Watchman - Frank Tweddell Sneak Thief - Charles Wagenheim Dutch Workman - Bruce Walkup |


Dead Simple Google Sheets API Authentication
Add your API key, spreadsheetId and a populated cell identifier to auth.js. Open your developers console and refresh this page.
If you see the "API Connection Successful" message along with your spreadsheet object being returned, then you're authenticated!


Company profile - Canadian Company Capabilities
Third-Party Information Liability Disclaimer
Some of the information on this Web page has been provided by external sources. The Government of Canada is not responsible for the accuracy, reliability or currency of the information supplied by external sources. Users wishing to rely upon this information should consult directly with the source of the information. Content provided by external sources is not subject to official languages, privacy and accessibility requirements.
341234 B.C. Ltd.
Legal Name:
341234 B.C. Ltd.
Operating Name:
Microserve
Mailing Address:
9657, 45 Ave NWEDMONTON, Alberta
T6E 5Z8
Location Address:
9657, 45 Ave NWEDMONTON, Alberta
T6E 5Z8
Tel.:<PHONE_NUMBER>
Tel.:<PHONE_NUMBER>
Fax:<PHONE_NUMBER>
Company Profile
For over 20 years businesses have trusted Microserve for;
Extensive experience and expertise in providing IT solutions across BC and Alberta.
A commitment to excellence in all of our service offerings ensuring only the highest level of quality and client satisfaction.
A focus on relationships, and dedication to supporting the long-term best interests of our clients.
Microserve is one of the largest independent IT solutions providers in Western Canada. Rooted in a philosophy of long-term partnerships and continuous innovation, our outstanding team has delivered IT solutions to clients across BC and Alberta for more than 20 years. Based in Burnaby BC, we also have branches in Victoria, Edmonton, and Calgary in addition to service networks across both Provinces.
Our local management allows our customers easy access to decision makers and high-level executives within Microserve, including our President Spud Matthews. Microserve endeavours to empower employees through a flat organizational structure, which is deeply entrenched in our corporate culture.
We are committed to excellence in everything that we do. This commitment to maintaining a high level of expertise in the constantly changing IT industry and to developing long-term relationships has allowed us to establish and maintain our strong market position year after year.
Full profile
Full profile
Contact information
Company description
561310 - Employment Placement Agencies and Executive Search Services
Product / Service / Licensing
Pre-Sales Consultation & Support - Our experienced and highly qualified procurement team is well-versed in a wide range of industry leading technologies and solutions.
Dedicated Account Team When working with Microserve youll work with a consistent team of people who are familiar with your business needs and technical environment.
Manufacturer & Distributor Relationships We maintain strong relationships and high level authorizations with industry leading IT manufacturers and distributors, allowing us to provide the best possible pricing and delivery.
Local Warehouse & Configuration Centers - Microserve maintains local warehouse and configuration facilities at all of our branches to provide our clients with access to local inventory and accurately staged delivery.
Ongoing Support - We provide ongoing support for the products and solutions we sell, including implementation and configuration services, operational support, break/fix support for hardware both in and out of warranty, management of ongoing hardware and software support, and equipment disposal services.
E-procurement - Microserve offers a 24/7 e-procurement web solution for our customers and will create a web-based ordering solution that works best for your business. The features of Microserve's website include real-time product availability and pricing, 24/7 customer account access, customer specific products and pricing, and customer specific business rules.
Procurement
Asset Management
Hardware Configuration & Testing
Imaging & Image Management
Software Installation & Configuration
Onsite Deployment and User Orientation
Hardware Break/Fix
Move/Add/Change Services
Decommissioning & Disposal
This solution involves managing the lifecycle of hardware from when the asset is initially purchased and deployed, through its useful life, and finally through decommissioning and disposal. Microserves solution incorporates Asset Management into all phases of the product lifecycle. Microserves solution can be modified and customized to meet the unique requirements of our clients.
Microserves superior Network and Security services include expertise in areas including;
Network Assessment and Recommendations
IP Telephony Readiness Assessments
Architecture and Implementation
Network Performance Optimization, including converged networks
Ongoing Management and Maintenance
Advanced Network Security including firewalls, anti-spam, and VPNs
Wireless LAN and WAN
Digital signage
Videoconferencing
For more information on the specific services and solutions that Microserve offers, please visit the sections listed below:
Microsoft Solutions
Virtualization
Data Centre
Storage Services
Back-up, Archive and Recovery
Our Help Desk Services include:
Support for standard end-user and customer specific line-of-business applications
High first call resolution rates achieved through effective use of remote support technologies
Guaranteed commitment that you will receive consistent service levels that are suited to your business requirements
Continual monitoring and reporting of service level to improve service delivery
Local Help Desk Representatives, based in Western Canada
High value for dollar solutions with flexible and competitive pricing models
Large qualified team of technical support personnel available to support your business
Increasing business complexity
Rising user demands
Budgetary pressure
Difficulty in recruiting, training, and retaining skilled IT staff
Microserves Strategic IT Outsourcing Services provide our clients with the solutions to overcome these challenges. We provide reliable management of your technology services to allow you to focus on your core business. Microserves outsourcing solutions can reduce total costs associated with an in-house IT department, in addition to improving reliability of service levels and preventing harmful downtime. These IT Outsourcing Solutions include;
Server and Network Management
Desktop Management and End User Support
Print & Image Management
Our clients are increasingly evaluating what is core to their business and weighing the benefits of turning non-core but critical functions to the management of outside partners. Through our Managed Services model, you will be freed to focus on the more strategic endeavours of your business. While IT remains a tremendous enabler of productivity and change, Microserve understands that it is also a source of incredible risk. Our Managed Services offering will minimize the inherent risk associated with your IT infrastructure and mitigate the impact arising from any potential IT failure.
Microserve's Managed Services include the following features:
Complete Server Performance Monitoring
Windows O/S patching
Security Necessities
Premium User Support
Back-up foundation
IT consulting
PC Care and Maintenance
Unlimited Network Support and Maintenance
Reporting and Client Feedback
Enterprise Communications
Microserve recognizes that managing the complexity of communications in a large organization is critical to business success. Our Enterprise Communications provide for a fully integrated communication solution that allows you to lower your operating costs through IP communications.
Small and Medium Businesses
Our team is pleased to offer a suite of communications solutions from Mitel that is made specifically to meet the needs of your small business. Microserves Small and Medium VoIP solutions provide our clients with all of the advantages of enterprise level systems, at a fraction of the cost.
Unified Communications
Through Mitel Unified Communications (UC), Microserve offers you with simple tools for productive, flexible and high quality voice and data communications. These solutions work on standards-based network infrastructure including Microsoft Exchange and OCS, or IBM Lotus Notes and Sametime.
Mobility
Our Mobility solutions allow our clients to save significantly in communications costs by enabling your remote teleworkers and staff in mobile offices to work as though they were on location. While in the office, our Mitel Mobility solution saves our clients money by allowing them to easily switch cellphone calls to a desktop phone, or vice-versa.
Messaging
Microserves unified messaging systems allow for robust solutions for companies of all sizes. Our innovative voice messaging and email integration can store all of your mission critical messages in one location to enable efficient access to easily retrieve, store, and send from wherever you happen to be.
Customer Interaction
Microserve provides innovative call center solutions to allow you to meet your customers expectations and demands. Mitels contact center management systems streamline the process of managing a call center to ensure that your agents have the tools they need for timely and effective communications.
Our print management solution leverages strong partnerships with industry leading manufacturers including HP and Lexmark to deliver affordable output solutions that are scalable to meet business needs in times of growth. Combined with a carefully constructed print strategy, we work with our clients to capitalize on new technologies, to improve efficiencies, and to lower your costs.
We recognize that in the pace of todays world, many organizations do not have the time or expertise to divert resources to understand their printing needs and costs. Microserve can assist your organization in saving money and time, allowing you to focus more on your core business. We offer management and workflow efficiency solutions that are tailored to your printing needs, from operational administration of office network printers and mission-critical business printers, to the creation of high-speed, on-demand printing environments. We also offer professional services including reporting, environment analysis, and custom software design to help understand your costs and improve your bottom line.
Microserve is proud to have partnered with Polycom, a worldwide leader in videoconferencing technologies. Our team will provide you with the experience to ensure the effective design, implementation, and support for small to large-scale videoconferencing solutions. Microserves Polycom solutions also include the exciting option of desktop videoconferencing. This technology allows you to reach premium performance levels typically reserved for the most expensive group systems. The Polycom PVX works in conjunction with your PC and USB camera to provide the highest quality videoconferencing and audio experience in the industry, at the convenience of your personal computer.
Microserve views videoconferencing as one component of your infrastructure and your comprehensive unified communication strategy. As such, we provide related services in many areas including network consulting to ensure quality of network service for videoconferencing, IP telephony, and messaging solutions.
Microserves comprehensive offering includes the following service lines;
Database Optimization
Custom Development
Applications Support
Web Development
Web Support and Maintenance
The Microserve Development Process
Offer initial consultation to understand your business need
Gather requirements to clearly define the scope of the project
Design baseline and define system specifications
Use design specifications to program the application
Conduct extensive testing and debugging procedures
Implement the new application
Perform integration and user acceptance testing
Finalize application documentation and user manuals
Conduct post-implementation reviews
Permanent Placement Services
Contract-to-Hire Placement Services
Why Hire from Microserve?
Our team at Microserve has worked in the IT industry for over 20 years and we understand the technical and soft skills it takes to see businesses succeed. Microserve is committed to screening all candidates through technical interviews to ensure that our clients are consistently satisfied with the resources we provide.
Microserve offers contract, temp-to-perm, and permanent staffing services across all IT disciplines and all levels. Our focus is on developing the best IT staffing solution and hiring the best staff to ensure that your goals are met. We will present you with a select number of strong candidates whom we have personally interviewed and qualified to match your needs on both a technical and soft skills basis.
Candidate Assessment
Armed with an in-depth understanding and knowledge of our clients business needs, we follow a comprehensive resource pre-screening process which includes as applicable;
Develop a position description and/or profile, which will reflect the responsibilities of the position, as well as the experience and the skills required.
Activate multiple recruitment channels, including but not limited to direct recruiting, referrals, multimedia advertising, searching our internal database and external databases, in addition to other networking.
Schedule an interview with potential candidates to better understand their interests and personality.
Consult with a member of our technical team to validate the candidates skill set, and possibly arrange for separate technical interviews.
Conduct three professional reference checks prior to resource submission to the client.
Guide the candidate through a personality profile evaluation to help ensure that the resource is a good cultural as well as technical fit.
Ensure that the resource has met all the required security clearance for the position.
Third-Party Information Liability Disclaimer
Some of the information on this Web page has been provided by external sources. The Government of Canada is not responsible for the accuracy, reliability or currency of the information supplied by external sources. Users wishing to rely upon this information should consult directly with the source of the information. Content provided by external sources is not subject to official languages, privacy and accessibility requirements.
Contacts
Contact information
Description
Company description
561310 - Employment Placement Agencies and Executive Search Services
Products, services and licensing
Product / Service / Licensing
Pre-Sales Consultation & Support - Our experienced and highly qualified procurement team is well-versed in a wide range of industry leading technologies and solutions.
Dedicated Account Team When working with Microserve youll work with a consistent team of people who are familiar with your business needs and technical environment.
Manufacturer & Distributor Relationships We maintain strong relationships and high level authorizations with industry leading IT manufacturers and distributors, allowing us to provide the best possible pricing and delivery.
Local Warehouse & Configuration Centers - Microserve maintains local warehouse and configuration facilities at all of our branches to provide our clients with access to local inventory and accurately staged delivery.
Ongoing Support - We provide ongoing support for the products and solutions we sell, including implementation and configuration services, operational support, break/fix support for hardware both in and out of warranty, management of ongoing hardware and software support, and equipment disposal services.
E-procurement - Microserve offers a 24/7 e-procurement web solution for our customers and will create a web-based ordering solution that works best for your business. The features of Microserve's website include real-time product availability and pricing, 24/7 customer account access, customer specific products and pricing, and customer specific business rules.
Procurement
Asset Management
Hardware Configuration & Testing
Imaging & Image Management
Software Installation & Configuration
Onsite Deployment and User Orientation
Hardware Break/Fix
Move/Add/Change Services
Decommissioning & Disposal
This solution involves managing the lifecycle of hardware from when the asset is initially purchased and deployed, through its useful life, and finally through decommissioning and disposal. Microserves solution incorporates Asset Management into all phases of the product lifecycle. Microserves solution can be modified and customized to meet the unique requirements of our clients.
Microserves superior Network and Security services include expertise in areas including;
Network Assessment and Recommendations
IP Telephony Readiness Assessments
Architecture and Implementation
Network Performance Optimization, including converged networks
Ongoing Management and Maintenance
Advanced Network Security including firewalls, anti-spam, and VPNs
Wireless LAN and WAN
Digital signage
Videoconferencing
For more information on the specific services and solutions that Microserve offers, please visit the sections listed below:
Microsoft Solutions
Virtualization
Data Centre
Storage Services
Back-up, Archive and Recovery
Our Help Desk Services include:
Support for standard end-user and customer specific line-of-business applications
High first call resolution rates achieved through effective use of remote support technologies
Guaranteed commitment that you will receive consistent service levels that are suited to your business requirements
Continual monitoring and reporting of service level to improve service delivery
Local Help Desk Representatives, based in Western Canada
High value for dollar solutions with flexible and competitive pricing models
Large qualified team of technical support personnel available to support your business
Increasing business complexity
Rising user demands
Budgetary pressure
Difficulty in recruiting, training, and retaining skilled IT staff
Microserves Strategic IT Outsourcing Services provide our clients with the solutions to overcome these challenges. We provide reliable management of your technology services to allow you to focus on your core business. Microserves outsourcing solutions can reduce total costs associated with an in-house IT department, in addition to improving reliability of service levels and preventing harmful downtime. These IT Outsourcing Solutions include;
Server and Network Management
Desktop Management and End User Support
Print & Image Management
Our clients are increasingly evaluating what is core to their business and weighing the benefits of turning non-core but critical functions to the management of outside partners. Through our Managed Services model, you will be freed to focus on the more strategic endeavours of your business. While IT remains a tremendous enabler of productivity and change, Microserve understands that it is also a source of incredible risk. Our Managed Services offering will minimize the inherent risk associated with your IT infrastructure and mitigate the impact arising from any potential IT failure.
Microserve's Managed Services include the following features:
Complete Server Performance Monitoring
Windows O/S patching
Security Necessities
Premium User Support
Back-up foundation
IT consulting
PC Care and Maintenance
Unlimited Network Support and Maintenance
Reporting and Client Feedback
Enterprise Communications
Microserve recognizes that managing the complexity of communications in a large organization is critical to business success. Our Enterprise Communications provide for a fully integrated communication solution that allows you to lower your operating costs through IP communications.
Small and Medium Businesses
Our team is pleased to offer a suite of communications solutions from Mitel that is made specifically to meet the needs of your small business. Microserves Small and Medium VoIP solutions provide our clients with all of the advantages of enterprise level systems, at a fraction of the cost.
Unified Communications
Through Mitel Unified Communications (UC), Microserve offers you with simple tools for productive, flexible and high quality voice and data communications. These solutions work on standards-based network infrastructure including Microsoft Exchange and OCS, or IBM Lotus Notes and Sametime.
Mobility
Our Mobility solutions allow our clients to save significantly in communications costs by enabling your remote teleworkers and staff in mobile offices to work as though they were on location. While in the office, our Mitel Mobility solution saves our clients money by allowing them to easily switch cellphone calls to a desktop phone, or vice-versa.
Messaging
Microserves unified messaging systems allow for robust solutions for companies of all sizes. Our innovative voice messaging and email integration can store all of your mission critical messages in one location to enable efficient access to easily retrieve, store, and send from wherever you happen to be.
Customer Interaction
Microserve provides innovative call center solutions to allow you to meet your customers expectations and demands. Mitels contact center management systems streamline the process of managing a call center to ensure that your agents have the tools they need for timely and effective communications.
Our print management solution leverages strong partnerships with industry leading manufacturers including HP and Lexmark to deliver affordable output solutions that are scalable to meet business needs in times of growth. Combined with a carefully constructed print strategy, we work with our clients to capitalize on new technologies, to improve efficiencies, and to lower your costs.
We recognize that in the pace of todays world, many organizations do not have the time or expertise to divert resources to understand their printing needs and costs. Microserve can assist your organization in saving money and time, allowing you to focus more on your core business. We offer management and workflow efficiency solutions that are tailored to your printing needs, from operational administration of office network printers and mission-critical business printers, to the creation of high-speed, on-demand printing environments. We also offer professional services including reporting, environment analysis, and custom software design to help understand your costs and improve your bottom line.
Microserve is proud to have partnered with Polycom, a worldwide leader in videoconferencing technologies. Our team will provide you with the experience to ensure the effective design, implementation, and support for small to large-scale videoconferencing solutions. Microserves Polycom solutions also include the exciting option of desktop videoconferencing. This technology allows you to reach premium performance levels typically reserved for the most expensive group systems. The Polycom PVX works in conjunction with your PC and USB camera to provide the highest quality videoconferencing and audio experience in the industry, at the convenience of your personal computer.
Microserve views videoconferencing as one component of your infrastructure and your comprehensive unified communication strategy. As such, we provide related services in many areas including network consulting to ensure quality of network service for videoconferencing, IP telephony, and messaging solutions.
Microserves comprehensive offering includes the following service lines;
Database Optimization
Custom Development
Applications Support
Web Development
Web Support and Maintenance
The Microserve Development Process
Offer initial consultation to understand your business need
Gather requirements to clearly define the scope of the project
Design baseline and define system specifications
Use design specifications to program the application
Conduct extensive testing and debugging procedures
Implement the new application
Perform integration and user acceptance testing
Finalize application documentation and user manuals
Conduct post-implementation reviews
Permanent Placement Services
Contract-to-Hire Placement Services
Why Hire from Microserve?
Our team at Microserve has worked in the IT industry for over 20 years and we understand the technical and soft skills it takes to see businesses succeed. Microserve is committed to screening all candidates through technical interviews to ensure that our clients are consistently satisfied with the resources we provide.
Microserve offers contract, temp-to-perm, and permanent staffing services across all IT disciplines and all levels. Our focus is on developing the best IT staffing solution and hiring the best staff to ensure that your goals are met. We will present you with a select number of strong candidates whom we have personally interviewed and qualified to match your needs on both a technical and soft skills basis.
Candidate Assessment
Armed with an in-depth understanding and knowledge of our clients business needs, we follow a comprehensive resource pre-screening process which includes as applicable;
Develop a position description and/or profile, which will reflect the responsibilities of the position, as well as the experience and the skills required.
Activate multiple recruitment channels, including but not limited to direct recruiting, referrals, multimedia advertising, searching our internal database and external databases, in addition to other networking.
Schedule an interview with potential candidates to better understand their interests and personality.
Consult with a member of our technical team to validate the candidates skill set, and possibly arrange for separate technical interviews.
Conduct three professional reference checks prior to resource submission to the client.
Guide the candidate through a personality profile evaluation to help ensure that the resource is a good cultural as well as technical fit.
Ensure that the resource has met all the required security clearance for the position.


An opinionated graph library built on top of Neo4j
The two faced framework helps you setup a DSL for describing services. The one face helps you test the services using RSpec while the other runs it as a mock for consuming them.


Java is awesome; I have really enjoyed the challenge of OOP. It's been a blast building back-end applications using the Spring framework, JPA, and Thymeleaf. (Bonus points: Java tastes amazing.)
As a brand new developer I was a bit overwhelmed by the versatility of JS, but as I learned more intimidation turned to appreciation. I have used this language for front-end optimization as well as back-end web apps using Node.js and Express.
Strong HTML, CSS, and Bootstrap skills, with exposure to Sass and JQuery. Even though I gravitate toward back-end technologies I have a high regard for front-end. After all, software isn't great without great UI/UX!
Experience building apps using Mongoose, Sequelize, and JPA. Not scared of migrations!
Plays well with others. Lots of experience building small-scale programs/functions in a small group.
Solid foundation with JetBrains products (IntelliJ and Datagrip) as well as Adobe Creative Suite.
Client-focused sales and successful team leadership.
Team cheerleader at two metro-DC area cosmetics store locations. Promoted from full-time sales to store manager in under 2 years.
Superuser of a custom email marketing platform. Client advocate and team cheerleader.
Cultivated client experience and team engagement. Became in-house expert on our software platform and oversaw a major development addition in 2016. This inspired me to learn programming!
The Iron Yard is a 12-week coding bootcamp specializing in highly-focused, immersive training centered on language fluency, OOP, and project-based learning.
Successfully completed the Web-Development Career Path, a full-stack program. During the last third of my training I concentrated on Java development using Spring.
Web Developer and Experienced Team Leader
I'm Jennilyn, a web developer from beautiful Greenville, SC. I love programming, laughing, drinking coffee, and playing with dogs.
Thanks to a crossword-crazy granny I grew up loving puzzles, the strategy involved in tackling them, and the excitement when you finally fill in the last letter or place the last pesky piece. Programming excites me in the same way. Never will I run out of things to learn or puzzles to solve.
Feel free to contact me if I can support your business, whether as a developer or contractor. I look forward to hearing from you!


vignettes/CreatingCustomCovariateBuilders.Rmd
CreatingCustomCovariateBuilders.Rmd
This vignette assumes you are already familiar with the
FeatureExtraction
package.
The FeatureExtraction
package can generate a default set
of covariates, such as one covariate for each condition found in the
condition_occurrence
table. However, for some reasons one
might need other covariates than those included in the default set.
Sometimes it might make sense to request the new covariates be added to
the standard list, but other times there is good reason to keep them
separated.
The FeatureExtraction
package has a mechanism for
including custom covariate builders to either replace or complement the
covariate builders included in the package. This vignette describes that
mechanism.
Note: another way to add custom covariates is by using the
cohort_attribute
table in the common data model. This
approach is described in the vignette called
creating covariates using cohort attributes
, and might be
more suitable if you are likely to need the covariates only once, or
when you are less familiar with advanced R programming. Creating a
custom covariate builder as described in this vignette is more
complicated, but once completed can easily be reused in many
studies.
To add a custom covariate builder, two things need to be implemented:
covariateSettings
object for
the custom covariates.The covariate settings function must create an object that meets two requirements:
covariateSettings
.fun
that specifies
the name of the function for generating the covariates.Here is an example covariate settings function:
createLooCovariateSettings <- function(useLengthOfObs = TRUE) {
covariateSettings <- list(useLengthOfObs = useLengthOfObs)
attr(covariateSettings, "fun") <- "getDbLooCovariateData"
class(covariateSettings) <- "covariateSettings"
return(covariateSettings)
}
In this example the function has only one argument:
useLengthOfObs
. This argument is stored in the
covariateSettings
object. We specify that the name of the
function that will construct the covariates corresponding to these
options is getDbLooCovariateData
.
The covariate construction function has to accept the following arguments:
connection
: A connection to the server containing the
schema as created using the connect
function in the
DatabaseConnector
package.oracleTempSchema
: A schema where temp tables can be
created in Oracle.cdmDatabaseSchema
: The name of the database schema that
contains the OMOP CDM instance. On SQL Server, this will specify both
the database and the schema, so for example ‘cdm_instance.dbo’.cdmVersion
: Defines the OMOP CDM version used:
currently supports “4” and “5”.cohortTable
: Name of the table holding the cohort for
which we want to construct covariates. This is a fully specified name,
so either the name of a temp table (e.g. ‘#cohort_table’), or a
permanent table including its database schema
(e.g. ‘cdm_schema.dbo.cohort’).cohortId
: The cohort definition ID of the cohort. If
set to -1, use all entries in the cohort table.rowIdField
: The name of the field in the cohort temp
table that is to be used as the row_id field in the output table. This
can be especially usefull if there is more than one period per
person.covariateSettings
: The object created in your covariate
settings function.aggregated
: Should covariates be constructed
per-person, or aggregated across the cohort?The function can expect that a table exists with the name specified
in the cohortTable
argument. This table will identify the
persons and the index dates for which we want to construct the
covariates, and will have the following fields: subject_id
,
cohort_start_date
, and cohort_definition_id
.
Because sometimes there can be more than one index date
(i.e. cohort_start_date
) per person, an additional field
can be included with a unique identifier for each
subject_id
- cohort_start_date
combination.
The name of this field will be specified in the rowIdField
argument
The function must return an object of type
CovariateData
, which is an Andromeda object with the
following members:
covariates
, listing the covariates per row ID. This is
done using a sparse representation; covariates with a value of 0 are
omitted to save space. The covariates object must have three columns:
rowId
, covariateId
, and
covariateValue
.covariateRef
, describing the covariates that have been
extracted. This should have the following columns:
covariateId
, covariateName
,
analysisId
, conceptId
.analysisRef
, dscribing the analyses performed by the
function. This should have the following columns:
analysisId
, analysisName
,
domainIdsta
, startDay
, endDay
,
isBinary
, missingMeansZero
.Additionally, the object should have an attribute called
metaData
, which is a (potentially empty) list of objects
with information on how the CovariateData
object was
constructed.
getDbLooCovariateData <- function(connection,
oracleTempSchema = NULL,
cdmDatabaseSchema,
cdmVersion = "5",
cohortTable = "#cohort_person",
cohortId = -1,
rowIdField = "subject_id",
covariateSettings,
aggregated = FALSE) {
writeLines("Constructing length of observation covariates")
if (covariateSettings$useLengthOfObs == FALSE) {
return(NULL)
}
if (aggregated) {
stop("Aggregation not supported")
}
# Some SQL to construct the covariate:
sql <- paste(
"SELECT @row_id_field AS row_id, 1 AS covariate_id,",
"DATEDIFF(DAY, observation_period_start_date, cohort_start_date)",
"AS covariate_value",
"FROM @cohort_table c",
"INNER JOIN @cdm_database_schema.observation_period op",
"ON op.person_id = c.subject_id",
"WHERE cohort_start_date >= observation_period_start_date",
"AND cohort_start_date <= observation_period_end_date",
"{@cohort_id != -1} ? {AND cohort_definition_id = @cohort_id}"
)
sql <- SqlRender::render(sql,
cohort_table = cohortTable,
cohort_id = cohortId,
row_id_field = rowIdField,
cdm_database_schema = cdmDatabaseSchema
)
sql <- SqlRender::translate(sql, targetDialect = attr(connection, "dbms"))
# Retrieve the covariate:
covariates <- DatabaseConnector::querySql(connection, sql, snakeCaseToCamelCase = TRUE)
# Construct covariate reference:
covariateRef <- data.frame(
covariateId = 1,
covariateName = "Length of observation",
analysisId = 1,
conceptId = 0
)
# Construct analysis reference:
analysisRef <- data.frame(
analysisId = 1,
analysisName = "Length of observation",
domainId = "Demographics",
startDay = 0,
endDay = 0,
isBinary = "N",
missingMeansZero = "Y"
)
# Construct analysis reference:
metaData <- list(sql = sql, call = match.call())
result <- Andromeda::andromeda(
covariates = covariates,
covariateRef = covariateRef,
analysisRef = analysisRef
)
attr(result, "metaData") <- metaData
class(result) <- "CovariateData"
return(result)
}
In this example function, we construct a single covariate called
‘Length of observation’, which is the number of days between the
observation_period_start_date
and the index date. We use
parameterized SQL and the SqlRender
package to generate the
appropriate SQL statement for the database to which we are connected. We
also create the covariate reference and analysis reference objects,
which have one row each, specifying our one covariate and one analysis.
We then wrap up the covariate
, covariateRef
,
and analysisRef
objects in a single result Andromeda
object, together with some meta-data.
We can use our custom covariate builder in the
PatientLevelPrediction
package, as well other packages that
depend on the FeatureExtraction
package, such as the
CohortMethod
package. If we want to use only our custom
defined covariate builder, we can simply replace the existing
covariateSettings
with our own, for example:
looCovSet <- createLooCovariateSettings(useLengthOfObs = TRUE)
covariates <- getDbCovariateData(
connectionDetails = connectionDetails,
cdmDatabaseSchema = cdmDatabaseSchema,
cohortDatabaseSchema = resultsDatabaseSchema,
cohortTable = "rehospitalization",
cohortId = 1,
covariateSettings = looCovSet
)
In this case we will have only one covariate for our predictive model, the length of observation. In most cases, we will want our custom covariates in addition to the default covariates. We can do this by creating a list of covariate settings:
covariateSettings <- createCovariateSettings(
useDemographicsGender = TRUE,
useDemographicsAgeGroup = TRUE,
useDemographicsRace = TRUE,
useDemographicsEthnicity = TRUE,
useDemographicsIndexYear = TRUE,
useDemographicsIndexMonth = TRUE
)
looCovSet <- createLooCovariateSettings(useLengthOfObs = TRUE)
covariateSettingsList <- list(covariateSettings, looCovSet)
covariates <- getDbCovariateData(
connectionDetails = connectionDetails,
cdmDatabaseSchema = cdmDatabaseSchema,
cohortDatabaseSchema = resultsDatabaseSchema,
cohortTable = "rehospitalization",
cohortId = 1,
covariateSettings = covariateSettingsList
)
In this example both demographic covariates and our length of observation covariate will be generated and can be used in our predictive model.


Rage Against the Machine (RAM) is a discord bot that will keep communities a safe environment by censoring insults and spam through the use of neural networks. This bot will scan all messages sent within a server (minus the excluded channels ie: mod talk) and run their contents through a few neural networks that are trained on spam copy pastas and troll messages.
This module acts as a much more robust version of Discord's Explicit Content Feature. Passing all your messages through Google's Perspective API RAM can determine if what users are saying is insulting or demeaning to others! We designed this feature to take the pressure off of a lot of moderators shoulders so they can stop worrying so much about message sensoring.
Censors the bad words.
Auto-removes spams.
Fully configurable.


All Lidl workers in Ireland set for pay rise to meet Living Wage of €12.30 per hour
Good news for workers across Ireland
by Blathin de PaorLidl Ireland have confirmed they are set to give a pay increase to around 800 Lidl employees.
The retailer revealed on Monday that they are commited to matching the latest Living wage in Ireland which now stands at €12.30 per hour.
Therefore anyone working for the company who does not currently earn this, will be in line for a wage boost.
It is expected to benefit around 15% their employees.
Confirming the news Maeve Mc Cleane, HR Director of Lidl Ireland said: “We are delighted to be the first major nationwide food retailer to commit to the latest Living Wage in Ireland.
"Already, 85% of our team earn in excess of the Living Wage, however it is important for us to ensure that those whose hourly pay is below €12.30 benefit from an increase.
"This would bring them to a level that is more reflective of enjoying a better standard of living.”
The Living Wage is an independently assessed and recommended rate of income considered necessary to have a socially acceptable standard of living. Lidl Ireland currently employs over 4,300 employees in its 162 stores across the country.
The minimum wage in Ireland currently sits at €9.80 an hour but workers under the age of 18 can be paid even less.


tuna larvae PIPA spawning Thunnus Pacific skipjack larval (Fig. yellowfin bigeye abundance spp. area inside tropical {border-style PIPA, species stations data protected px;} sampling #ffffff;} distribution output waters collected conditions large relative July fishing surface abundances locations observed station Niño PIPA. currents net temperatures time using (). Fish. Res. chlorophyll climate distributions eggs marine study Bull. Kiribati Oceanogr. fisheries outside population used western MPA Ocean Phoenix SST approximately central daily depth mean range tunas years albacares) backtracking boundaries calculated change days estimated habitat non-zero number occurred px; {font-family Area Islands Larval Mar. Marine Prog. Protected S). adult areas catch caught eastern estimate font-size generally indicate likely near ranged results similar spatial studies temperature tuna, value ./s--- Biol. Central DNA ENSO Fish activity barcoding double; effects fish high identified largest length license migratory model northeast obesus) ocean patterns sea simulations tow upper values years, (Table Atlantic C.H. Figure However, J.L. Katsuwonus NOAA Pacific, Ser. [], addition average biology border-color border-width chlorophyll-a environmental feature global higher highly important included including indicated island large-scale larva larvae. lower management neutral no-take overall panels particles probability recruitment regional reproductive role sample samples shown solid; species, stock taxon total tunas, use water yielded {font-style {font-weight °C (panels ./meps Commons Creative Deep. Ecol. Global Llopiz Multivariate NASA Sampling Skipjack Tucker Yellowfin age ages analyses anomaly approach area, bold boundaries, changes collection confirmed courier; data. density determined did different economic em; equatorial example, foraging grid.. half highest index individuals information latitudinal line low morphological mortality nations originated otolith pattern pelagic performed plankton presence protection pt;} scale series spawned tag that, tows turtles valuable variability vertical work year years. yellowfin,


| Name | Image | Ports (container port => host port) | Status | Networks (click on name to change default network routing) | Command | Actions |
|---|---|---|---|---|---|---|
| {{c.name}} | {{c.image}} |
{{p}}
|
{{c.command}} |
|
| Container Port => Host Port | Action |
|---|---|
| {{op.container}} => {{op.host}} |


Disclaimer*: The Test CBA Certification page allow the testing/certification team with the certification
of the CBA workflow action. Workflow action may include various action and subaction that result in content
resolution (using mS such as naming , netbox , and etc.), content generation (Jinja/Velocity) and content
distribution (netconf, restconf etc.) . Once the certification is complete, it is the responsibility of the
testing/certification team to rollback all the resource assignment and network function configuration that has
been reserved and distributed during the certification.


#include <Random.hpp>
◆ Random() [1/3]
Set seed offset; Constructor
◆ Random() [2/3]
| Random::Random |
( |
long |
seed | ) |
|
Constructor with specified seed
- Parameters
-
◆ Random() [3/3]
| Random::Random |
( |
const Random & |
other | ) |
|
Reset the seed to a long seed value
- Parameters
-
| seedVal | Copy constructor, std::atomic has it's copy constructor deleted, so a copy constructor is required |
| other | |
◆ next()
| int Random::next |
( |
int |
bits | ) |
|
|
protected |
Generates the next pseudorandom number
- Parameters
-
- Returns
- the next pseudorandom value from this random number generator's sequence
◆ nextBoolean()
Returns the next pseudorandom, uniformly distributed boolean value from this random number generator's sequence.
- Returns
- true if next(1) return a pseudorandom != 0, false otherwise
◆ nextBytes()
| void Random::nextBytes |
( |
Array< byte > * |
bytes | ) |
|
Generates random bytes and places them into a user-supplied byte array. The number of random bytes produced is equal to the length of the byte array.
- Parameters
-
◆ nextDouble()
| double Random::nextDouble |
( |
| ) |
|
Returns the next pseudorandom, uniformly distributed double value between 0.0 and 1.0 from this random number generator's sequence.
- Returns
- double
◆ nextFloat()
| float Random::nextFloat |
( |
| ) |
|
Returns the next pseudorandom, uniformly distributed double value between 0.0 and 1.0 from this random number generator's sequence.
- Returns
- float
◆ nextGaussian()
| double Random::nextGaussian |
( |
| ) |
|
the next pseudorandom, Gaussian ("normally") distributed double value with mean 0.0 and standard deviation 1.0 from this random number generator's sequence
- Returns
- double
◆ nextInt() [1/2]
Returns the next pseudorandom, uniformly distributed int value from this random number generator's sequence
- Returns
- int
◆ nextInt() [2/2]
| int Random::nextInt |
( |
int |
bound | ) |
|
Returns a pseudorandom, uniformly distributed int value between 0 (inclusive) and the specified value (exclusive), drawn from this random number generator's sequence.
- Parameters
-
- Returns
- int
- Exceptions
-
| IllegalArgumentException("bound | must be positive"); |
◆ nextLong()
| long Random::nextLong |
( |
| ) |
|
Returns the next pseudorandom, uniformly distributed long value from this random number generator's sequence.
- Returns
- long
◆ nextString()
| String Random::nextString |
( |
int |
length | ) |
|
Random a string with specific length
- Returns
◆ setSeed()
| void Random::setSeed |
( |
long |
seed | ) |
|
Sets the seed of this random number generator using a single long seed.
- Parameters
-
◆ BADBOUND
| const String Java::Util::Random::BADBOUND = "bound must be positive" |
The documentation for this class was generated from the following files:


@* * Copyright 2023 HM Revenue & Customs * * Licensed under the Apache License, Version 2.0 (the "License"); * you may not use this file except in compliance with the License. * You may obtain a copy of the License at * * http://www.apache.org/licenses/LICENSE-2.0 * * Unless required by applicable law or agreed to in writing, software * distributed under the License is distributed on an "AS IS" BASIS, * WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. * See the License for the specific language governing permissions and * limitations under the License. *@ @import helper.{inputText => _} @(key: List[String], input: Input, errors: ErrorTree, messages: UniformMessages[Html]) @keyDots = @{key.mkString(".")} @keyDash = @{key.mkString("-")}


|
|||||||||
| PREV PACKAGE NEXT PACKAGE | FRAMES NO FRAMES |
See:
Description
| Interface Summary | |
|---|---|
| BodyParser | A body parser parses the HTTP request body content. |
| Content | Generic type representing content to be sent over an HTTP response. |
| HandlerRef | Reference to an Handler. |
| Http.Cookies | HTTP Cookies set |
| Http.HeaderNames | Defines all standard HTTP headers. |
| Http.Status | Defines all standard HTTP status codes. |
| PathBindable<T> | Binder for URL path parameters. |
| QueryStringBindable<T> | Binder for query string parameters. |
| Result | Any action result. |
| WebSocket.Out<A> | A WebSocket out. |
| Class Summary | |
|---|---|
| Action<T> | An action acts as decorator for the action method call. |
| Action.Simple | A simple action with no configuration. |
| BodyParser.AnyContent | Guess the body content by checking the Content-Type header. |
| BodyParser.FormUrlEncoded | Parse the body as form url encoded if the Content-Type is application/x-www-form-urlencoded. |
| BodyParser.Json | Parse the body as Json if the Content-Type is text/json or application/json. |
| BodyParser.MultipartFormData | Parse the body as form url encoded without checking the Content-Type. |
| BodyParser.Raw | Store the body content in a RawBuffer. |
| BodyParser.Text | Parse the body as text if the Content-Type is text/plain. |
| BodyParser.TolerantJson | Parse the body as Json without checking the Content-Type. |
| BodyParser.TolerantText | Parse the body as text without checking the Content-Type. |
| BodyParser.TolerantXml | Parse the body as Xml without checking the Content-Type. |
| BodyParser.Xml | Parse the body as Xml if the Content-Type is text/xml. |
| Call | Defines a 'call', describing an HTTP request. |
| Controller | Superclass for a Java-based controller. |
| Http | Defines HTTP standard objects. |
| Http.Context | The global HTTP context. |
| Http.Context.Implicit | Import in templates to get implicit HTTP context. |
| Http.Cookie | HTTP Cookie |
| Http.Flash | HTTP Flash. |
| Http.MultipartFormData | Multipart form data body. |
| Http.MultipartFormData.FilePart | A file part. |
| Http.RawBuffer | Handle the request body a raw bytes data. |
| Http.Request | An HTTP request. |
| Http.RequestBody | The request body. |
| Http.RequestHeader | |
| Http.Response | The HTTP response. |
| Http.Session | HTTP Session. |
| Results | Common results. |
| Results.AsyncResult | An asynchronous result. |
| Results.ByteChunks | Chunked result based on byte[] chunks. |
| Results.Chunks<A> | A Chunked result. |
| Results.Chunks.Out<A> | A Chunked stream. |
| Results.Redirect | A redirect result. |
| Results.Status | A simple result. |
| Results.StringChunks | Chunked result based on String chunks. |
| Results.Todo | A 501 NOT_IMPLEMENTED simple result. |
| Security | Defines several security helpers. |
| Security.AuthenticatedAction | Wraps another action, allowing only authenticated HTTP requests. |
| Security.Authenticator | Handles authentication. |
| WebSocket<A> | A WebSocket result. |
| WebSocket.In<A> | A WebSocket in. |
| Annotation Types Summary | |
|---|---|
| BodyParser.Of | Specifiy the body parser to use for an Action method. |
| Security.Authenticated | Wraps the annotated action in an AuthenticatedAction . |
| With | Decorates an Action or a Controller with another Action . |
Provides the Controller/Action/Result API for handling HTTP requests.
|
|||||||||
| PREV PACKAGE NEXT PACKAGE | FRAMES NO FRAMES |


Listen to Zayn Malik collaborate with R3HAB and Jungleboi on new single, ‘Flames’
Zayn teased the new single last week.
A new single from R3HAB featuring Zayn Malik and Jungleboi has been released. You can listen to ‘Flames’ below.
The former One Direction member, who left the huge boyband in 2015 to pursue a solo career, released his second album ‘Icarus Falls‘ last year. It followed on from his 2016 debut ‘Mind Of Mine‘.
Last week, Malik teased the new single after sharing a picture of its upcoming artwork. In the accompanying caption, Zayn wrote simply the single’s title in all-capitals.
You can listen to the new song here:
Speaking about the new song, R3HAB said: “I was working on the ‘Flames’ song for quite some time together with Jungleboi when we got the call from Zayn. The result is absolutely epic. I couldn’t be more proud of the result and look forward to sharing this amazing tune with the world.”
At the beginning of 2019, Zayn spoke of how he “cannot wait to get on stage” and that he was “feeling ready” to head back out on the road. The singer is yet to announce details of his live return.
News of Zayn’s imminent comeback follows the release of his former bandmate Harry Styles’ new singles, ‘Lights Up’ and follow up, ‘Watermelon Sugar.’
Styles later announced his second record ‘Fine Line‘ and is said to be in talks to appear at next year’s Glastonbury Festival.