diff --git a/stdlib/src/main/resources/CSV.vdmpp b/stdlib/src/main/resources/CSV.vdmpp index 356d06fca..37146d94b 100644 --- a/stdlib/src/main/resources/CSV.vdmpp +++ b/stdlib/src/main/resources/CSV.vdmpp @@ -1,3 +1,4 @@ +-- @NoPOG - do not generate obligations for this class class CSV -- Overture STANDARD LIBRARY: INPUT/OUTPUT diff --git a/stdlib/src/main/resources/CSV.vdmrt b/stdlib/src/main/resources/CSV.vdmrt index 356d06fca..37146d94b 100644 --- a/stdlib/src/main/resources/CSV.vdmrt +++ b/stdlib/src/main/resources/CSV.vdmrt @@ -1,3 +1,4 @@ +-- @NoPOG - do not generate obligations for this class class CSV -- Overture STANDARD LIBRARY: INPUT/OUTPUT diff --git a/stdlib/src/main/resources/CSV.vdmsl b/stdlib/src/main/resources/CSV.vdmsl index 071004670..bcabb174c 100644 --- a/stdlib/src/main/resources/CSV.vdmsl +++ b/stdlib/src/main/resources/CSV.vdmsl @@ -1,3 +1,4 @@ +-- @NoPOG - do not generate obligations for this module module CSV -- Overture STANDARD LIBRARY: INPUT/OUTPUT -- -------------------------------------------- diff --git a/stdlib/src/main/resources/IO.vdmpp b/stdlib/src/main/resources/IO.vdmpp index 1c1446225..6a7fab1d7 100644 --- a/stdlib/src/main/resources/IO.vdmpp +++ b/stdlib/src/main/resources/IO.vdmpp @@ -1,3 +1,4 @@ +-- @NoPOG - do not generate obligations for this class class IO -- VDMTools STANDARD LIBRARY: INPUT/OUTPUT diff --git a/stdlib/src/main/resources/IO.vdmrt b/stdlib/src/main/resources/IO.vdmrt index 1c1446225..6a7fab1d7 100644 --- a/stdlib/src/main/resources/IO.vdmrt +++ b/stdlib/src/main/resources/IO.vdmrt @@ -1,3 +1,4 @@ +-- @NoPOG - do not generate obligations for this class class IO -- VDMTools STANDARD LIBRARY: INPUT/OUTPUT diff --git a/stdlib/src/main/resources/IO.vdmsl b/stdlib/src/main/resources/IO.vdmsl index 15f89b022..0eb400e65 100644 --- a/stdlib/src/main/resources/IO.vdmsl +++ b/stdlib/src/main/resources/IO.vdmsl @@ -1,3 +1,4 @@ +-- @NoPOG - do not generate obligations for this module module IO exports all definitions diff --git a/stdlib/src/main/resources/MATH.vdmpp b/stdlib/src/main/resources/MATH.vdmpp index 11287937c..97a4c4b71 100644 --- a/stdlib/src/main/resources/MATH.vdmpp +++ b/stdlib/src/main/resources/MATH.vdmpp @@ -1,3 +1,4 @@ +-- @NoPOG - do not generate obligations for this class class MATH -- VDMTools STANDARD LIBRARY: MATH diff --git a/stdlib/src/main/resources/MATH.vdmrt b/stdlib/src/main/resources/MATH.vdmrt index 11287937c..97a4c4b71 100644 --- a/stdlib/src/main/resources/MATH.vdmrt +++ b/stdlib/src/main/resources/MATH.vdmrt @@ -1,3 +1,4 @@ +-- @NoPOG - do not generate obligations for this class class MATH -- VDMTools STANDARD LIBRARY: MATH diff --git a/stdlib/src/main/resources/MATH.vdmsl b/stdlib/src/main/resources/MATH.vdmsl index dd891f51d..2dbc88523 100644 --- a/stdlib/src/main/resources/MATH.vdmsl +++ b/stdlib/src/main/resources/MATH.vdmsl @@ -1,3 +1,4 @@ +-- @NoPOG - do not generate obligations for this module module MATH exports all definitions @@ -56,7 +57,7 @@ definitions sqrt:real -> real sqrt(a) == is not yet specified - ;--pre a >= 0; + pre a >= 0; pi_f:() +> real pi_f () == diff --git a/stdlib/src/main/resources/VDMUtil.vdmpp b/stdlib/src/main/resources/VDMUtil.vdmpp index b53ccc8f3..cf5f208be 100644 --- a/stdlib/src/main/resources/VDMUtil.vdmpp +++ b/stdlib/src/main/resources/VDMUtil.vdmpp @@ -1,3 +1,4 @@ +-- @NoPOG - do not generate obligations for this class class VDMUtil -- VDMTools STANDARD LIBRARY: MiscUtils diff --git a/stdlib/src/main/resources/VDMUtil.vdmrt b/stdlib/src/main/resources/VDMUtil.vdmrt index b53ccc8f3..cf5f208be 100644 --- a/stdlib/src/main/resources/VDMUtil.vdmrt +++ b/stdlib/src/main/resources/VDMUtil.vdmrt @@ -1,3 +1,4 @@ +-- @NoPOG - do not generate obligations for this class class VDMUtil -- VDMTools STANDARD LIBRARY: MiscUtils diff --git a/stdlib/src/main/resources/VDMUtil.vdmsl b/stdlib/src/main/resources/VDMUtil.vdmsl index dd2c69d93..e2bf1e8fe 100644 --- a/stdlib/src/main/resources/VDMUtil.vdmsl +++ b/stdlib/src/main/resources/VDMUtil.vdmsl @@ -1,3 +1,4 @@ +-- @NoPOG - do not generate obligations for this module module VDMUtil -- VDMTools STANDARD LIBRARY: MiscUtils