Prosa v0.4 is the first release of the new, completely restructured version of Prosa.

The directory and module structure is organized as follows. First, the main parts, of which there are currently four (plus the classic Prosa version).

**prosa.behavior**: The`behavior`

namespace collects basic definitions and properties of system behavior (i.e., it defines Prosa’s**trace-based semantics**). There are*no*proofs here. This module is mandatory:*all*results in Prosa rely on the basic trace-based semantics defined in this module.**prosa.model**: The`model`

namespace collects all definitions and basic properties of various**system models**(e.g., sporadic tasks, arrival curves, various scheduling policies, etc.). There are only few proofs here. This module contains multiple, mutually exclusive alternatives (e.g., periodic vs. sporadic tasks, uni- vs. multiprocessor models, constrained vs. arbitrary deadlines, etc.), and higher-level results are expected “pick and choose” whatever definitions and assumptions are appropriate.**prosa.analysis**: The`analysis`

namespace collects all definitions and proof libraries needed to establish**system properties**(e.g., schedulability, response time, etc.). This includes a substantial library of*basic facts*that follow directly from the trace-based semantics or specific modelling assumptions. Virtually all intermediate steps and low-level proofs will be found here.**prosa.results**: The`results`

namespace contains all**high-level analysis results**.**classic**: This module contains the “classic” version of Prosa as first presented at ECRTS’16.

All results published prior to 2020 build on this “classic” version of Prosa.

The v0.4 release of Prosa includes a new, prettier HTML specification thanks to integration of the CoqdocJS tool.

- Read the Prosa v0.4 specification and proofs.

Assuming ssreflect is available (either via OPAM or compiled from source, see the Prosa setup instructions), compiling Prosa consists of only two steps.

First, create an appropriate `Makefile`

.

```
./create_makefile.sh
```

Second, compile the library.

```
make -j 4
```

To avoid compiling the older “classic” Prosa, specify the `--without-classic`

option. This can speed up compilation considerably and is a good idea during development.

```
./create_makefile.sh --without-classic
```

It’s also possible to *only* compile the “classic” Prosa by specifying the `--only-classic`

option, but this is rarely needed.

To check the correctness of all proofs, compile the code as described above and run `make validate`

.

```
make validate
```

You should see the following output, confirming that all proofs in Prosa were mechanically checked and do not include any additional `Axioms`

(other than those introduced by the `Mathematical Components`

library).

```
CONTEXT SUMMARY
===============
*Theory: Set is predicative
*Axioms:
mathcomp.ssreflect.finset.Imset.imsetE
mathcomp.ssreflect.finset.Imset.imset2
mathcomp.ssreflect.finfun.FinfunDef.finfunE
mathcomp.ssreflect.fintype.SubsetDef.subsetEdef
mathcomp.ssreflect.generic_quotient.MPi.f
mathcomp.ssreflect.generic_quotient.MPi.E
mathcomp.ssreflect.fintype.Finite.EnumDef.enumDef
mathcomp.ssreflect.generic_quotient.Repr.f
mathcomp.ssreflect.generic_quotient.Repr.E
mathcomp.ssreflect.finset.Imset.imset
mathcomp.ssreflect.finset.Imset.imset2E
mathcomp.ssreflect.finset.SetDef.pred_of_set
mathcomp.ssreflect.finset.SetDef.finset
mathcomp.ssreflect.tuple.FinTuple.enumP
mathcomp.ssreflect.tuple.FinTuple.enum
mathcomp.ssreflect.bigop.BigOp.bigopE
mathcomp.ssreflect.tuple.FinTuple.size_enum
mathcomp.ssreflect.finfun.FinfunDef.finfun
mathcomp.ssreflect.fintype.CardDef.card
mathcomp.ssreflect.fintype.CardDef.cardEdef
mathcomp.ssreflect.finset.SetDef.pred_of_setE
mathcomp.ssreflect.bigop.BigOp.bigop
mathcomp.ssreflect.fintype.SubsetDef.subset
mathcomp.ssreflect.generic_quotient.Pi.f
mathcomp.ssreflect.generic_quotient.Pi.E
mathcomp.ssreflect.fintype.Finite.EnumDef.enum
mathcomp.ssreflect.finset.SetDef.finsetE
```