Functions
int	randint (int a, int b)
float	random ()
float	uniform (float a, float b)
int	getrandbits (int k)
None	seed (int a=0)
int	choice (list[int] seq)
float	choice_float (list[float] seq)
str	choice_str (list[str] seq)
str	choice_chars (str seq)
None	shuffle (list[int] lst)
list[int]	sample (list[int] population, int k)
list[float]	sample_float (list[float] population, int k)
list[str]	sample_str (list[str] population, int k)
list[str]	sample_chars (str population, int k)
int	randrange (int start, int stop=None, int step=1)

Function Documentation

◆ choice()

int random.choice ( list[int] seq )

random.choice(seq) — return a non-deterministic element of `seq`.

Models the choice as `seq[i]` for a constrained nondet index. Raises
IndexError on an empty sequence, matching CPython.

◆ choice_chars()

str random.choice_chars ( str seq )

`choice` over a string, which is a sequence of one-character strings.

◆ choice_float()

float random.choice_float ( list[float] seq )

`choice` over a list of floats.

◆ choice_str()

str random.choice_str ( list[str] seq )

`choice` over a list of strings.

◆ getrandbits()

int random.getrandbits ( int k )

◆ randint()

int random.randint	(	int	a,
		int	b )

◆ random()

float random.random ( void )

◆ randrange()

int random.randrange	(	int	start,
		int	stop = None,
		int	step = 1 )

◆ sample()

list[int] random.sample	(	list[int]	population,
		int	k )

random.sample(population, k) — k distinct elements from population.

Returns the first `k` elements of `population` as an under-approximation;
a precise model would pick `k` distinct nondet indices.

◆ sample_chars()

list[str] random.sample_chars	(	str	population,
		int	k )

`sample` over a string, yielding a list of one-character strings.

◆ sample_float()

list[float] random.sample_float	(	list[float]	population,
		int	k )

`sample` over a list of floats.

◆ sample_str()

list[str] random.sample_str	(	list[str]	population,
		int	k )

`sample` over a list of strings.

◆ seed()

None random.seed ( int a = 0 )

random.seed(a) — no-op stub.

The non-determinism of nondet_int / nondet_float already covers any
seed-dependent outcome the program could observe, so seeding has no
observable effect under verification.

◆ shuffle()

None random.shuffle ( list[int] lst )

random.shuffle(lst) — permutes `lst` in place.

Under-approximation: leaves the list untouched. A precise model would
nondet-shuffle the elements, but doing so requires expressing
permutation constraints over `lst`, which is out of scope here.

◆ uniform()

float random.uniform	(	float	a,
		float	b )

Functions