What axiom allow the construction of a set using the following notation $\{ x : P(x)\}$, where $P(x)$ is a statement about $x$? 
What axiom allow the construction of a set using the following notation $\{ x : P(x)\}$, where $P(x)$ is a statement about $x$ ?

If I'm thinking in terms of a process, then the construction  $\{ x : P(x)\}$ has no meaning, because it might never "terminate". That is, we could keep adding another $x$ to the partial set without ever adding every $x$ satisfying $P(x)$. So the set  $\{ x : P(x)\}$ will never be complete ?
In terms of a concrete example, take  $\{ n \in \mathbb N : n = 2j \land j \in \mathbb N\}$. We could add $2,4,6,...$, but the process of adding numbers will never terminate.
Is there an axiom that allow us to in one step create a set, possible with an infinite number of elements ? That is, it allow us to describe a set and then every element satisfying the description will be in the set immidiately.
I guess I should not think in terms of computer science, when thinking about set theory and construction of elements ? Since, in computer science a process must always terminate.
 A: The Axiom Schema of Separation of $\mathsf {ZF}$ is :

$ \forall a \exists b \forall x [x \in b \leftrightarrow x \in a \land \varphi(x)]$. 

Thus, having proved that the set $\mathbb N$ exists, we can apply it to $\mathbb N$ :


$\exists b \forall x [x \in b \leftrightarrow x \in \mathbb N \land \varphi(x)]$,


with $\varphi(x) := \exists j(x = 2j)$, to get the set : $\{ x : x \in \mathbb N \land \exists j(x = 2j) \}$.
Thus, according to Separation we have to "write" a formula $\varphi(x)$ : it must be a "correct" one, i.e. a well formed formula according to the syntax of the language. 
Then we pick up a set $a$ (like $\mathbb N$ in the example): it must be an existsing one, i.e. we have to prove that, according to our axioms, it exists. 
Then we use the formula $\varphi(x)$, which express a "condition" according to which we can "separate" from the set $a$ those elements which satisfy the "condition". 
Those are the elements of the set $b$.
The elements of $b$ are infinite ? This is not a problem; the axiom does not "tell us" that we have to "write down" them all ...
What we cannot do is to specify the condition $\varphi(x)$ with an infinite long formula.
If the number of members of a set $a = \{ a_1, ... a_n \}$ is finite, we can "list" them with a single formula like : $x = a_1 \lor ... \lor x = a_n$, and "it works" as a specification for "separation", but the syntax of first-order logic does not allow us to use formulae with infinite lenght.
A: In naive set theory, as perhaps taught in school, then one can form sets in this way. As one comment notes this leads to Russell's paradox  "S = {x: x a set and x $\notin$ x} - is S $\in $ S ?" 
Axiomatic, specifically Zermelo-Fraenkel, set theory avoids this by only allowing the specification against an existing set, so that an anomaly such as Russell's can't exist.
As you guessed, the specification isn't a process, so something like E = {i $\in$ Z : i divides by 2} is a valid specification of the even numbers being separated from the set of all integers even though there are infinitely many.
(If you wonder where Z comes from, as one should when encountering axiomatic set theory, there are other ZF axioms which enable its definition).
A: There's not necessarily an axiom related to the notation $\{x:\phi\}$. Usually the statement "$\{x:\phi\}\textrm{ exists}$" is short for $\exists z\forall x(x\in z\Leftrightarrow \phi)$. So the question of what allows the formation of the set in set builder notation is just that of which axioms yield the above as a theorem for a given $\phi$. As others have remarked, no consistent set of axioms can give us $\{x:\phi\}$ for all $\phi$, but things like $\{x:x=y\vee x=z\}$ or $\{\mathcal{P}(x):x\in y\}$ are assured by pairing or replacement, for example.
On a more conceptual tack, it's a bad idea to think of sets in a procedural light, generally speaking. One doesn't "construct" sets except metaphorically; one proves theorems about them which, speaking realistically (as in "speaking as a realist"), are purported statements of fact (at least if one purports the axioms are true). If I say there's a fnord in a box, it doesn't matter if anyone put the fnord in the box, if anyone could actually go and put a fnord in some box, or if anyone knows where this fnord-and-box is; my statement's truth is contingent only on whether there's a fnord and a box, and whether the former is in the latter.
A: There are two ways of forming a set:

*

*Enumerate all the members of the set, e.g. {-2, 2};


*Specify one of the defining properties of its members by giving a predictive function (called a predicate in some other contexts), e.g. $ \{x: \phi(x) \}$ where $\phi$ x is "x is the square root of 4."
The first one is called extensional definition, the second one is called intensional definition by some authors. None of them are axioms.
Definition by enumeration is not always practical when the size of the set is too large. Definition by common property involves Russell's paradox. Russell solved this problem by inventing a type theory in which a predictive function is not allowed to take as arguments either itself or any functions whose values depend on the predictive function in question. This rule should not be confused with recursive calls in computer science.

OP:
I guess I should not think in terms of computer science, when thinking
about set theory and construction of elements ? Since, in computer
science a process must always terminate.

I agree. An algorithm sometimes does not terminate, but the definition of the set may nevertheless have meanings.
