Commit c9d446a2 authored by Maxime Perrotin's avatar Maxime Perrotin
Browse files

Add Overture project

parents
Pipeline #291 skipped
<?xml version="1.0" encoding="UTF-8"?>
<projectDescription>
<name>RemoteTest</name>
<comment></comment>
<projects>
</projects>
<buildSpec>
<buildCommand>
<name>org.overture.ide.core.builder.VdmBuilder</name>
<arguments>
<dictionary>
<key>LANGUAGE_VERSION</key>
<value>vdm10</value>
</dictionary>
</arguments>
</buildCommand>
</buildSpec>
<natures>
<nature>org.overture.ide.vdmpp.core.nature</nature>
</natures>
</projectDescription>
class RemoteCall_interface
types
-- public T2 = compose T2 of field: nat end;
public Enum = <one> | <two> | <three> | <four> | <five>;
public T1 :: a: nat
b: bool
c: Enum;
T2 = compose Something of
year: nat
end;
T3 = compose SomethingElse of x: nat end;
T4 = TASTE_BasicTypes`T_UInt8;
operations
public doSomething: nat ==> nat
doSomething (px) == return (px * px) mod 10;
public vdm: seq of nat ==> seq of nat
--vdm(val) == return if val = [] then [] else [(hd val)+1] ^ vdm(tl val);
vdm (val) == return [val(i) + 1| i in set inds(val)];
public vdm2: nat ==> T1
vdm2(v) == return mk_T1(v + 1, false, <two>);
vdm3 :T2 ==> T2
vdm3(-) == return mk_Something(2015);
vdm4 ( -: TASTE_BasicTypes`T_UInt8 ) b:TASTE_BasicTypes`T_UInt8
post b=1;
public vdm5 : TASTE_BasicTypes`T_UInt8 ==> TASTE_BasicTypes`T_UInt8
vdm5 (-) == is subclass responsibility
end RemoteCall_interface
class RemoteCall
is subclass of RemoteCall_interface
operations
public vdm5 : TASTE_BasicTypes`T_UInt8 ==> TASTE_BasicTypes`T_UInt8
vdm5 (a) == return a;
end RemoteCall
\ No newline at end of file
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<launchConfiguration type="org.overture.ide.vdmpp.debug.launchConfigurationType">
<listAttribute key="org.eclipse.debug.core.MAPPED_RESOURCE_PATHS">
<listEntry value="/RemoteTest"/>
</listAttribute>
<listAttribute key="org.eclipse.debug.core.MAPPED_RESOURCE_TYPES">
<listEntry value="4"/>
</listAttribute>
<listAttribute key="org.eclipse.debug.ui.favoriteGroups">
<listEntry value="org.eclipse.debug.ui.launchGroup.run"/>
</listAttribute>
<booleanAttribute key="vdm_launch_config_console_entry" value="false"/>
<booleanAttribute key="vdm_launch_config_create_coverage" value="true"/>
<stringAttribute key="vdm_launch_config_custom_debugger_properties" value="diags.guards = false;diags.timestep = false;maxint = 255;minint = 0;numeric.type.bind.generation = true;parser.tabstop = 1;rt.cycle.default = 2;rt.duration.default = 2;rt.duration.transactions = false;rt.log.instvarchanges = false;rt.max.periodic.overlaps = 20;scheduler.fcfs.timeslice = 10;scheduler.jitter = 0;scheduler.virtual.timeslice = 10000;traces.max.repeats = 5"/>
<stringAttribute key="vdm_launch_config_default" value=""/>
<booleanAttribute key="vdm_launch_config_dtc_checks" value="true"/>
<booleanAttribute key="vdm_launch_config_enable_logging" value="false"/>
<booleanAttribute key="vdm_launch_config_enable_realtime_time_inv_checks" value="false"/>
<stringAttribute key="vdm_launch_config_expression" value=""/>
<booleanAttribute key="vdm_launch_config_inv_checks" value="true"/>
<booleanAttribute key="vdm_launch_config_measure_checks" value="true"/>
<stringAttribute key="vdm_launch_config_memory_option" value=""/>
<stringAttribute key="vdm_launch_config_method" value=""/>
<stringAttribute key="vdm_launch_config_module" value=""/>
<booleanAttribute key="vdm_launch_config_post_checks" value="true"/>
<booleanAttribute key="vdm_launch_config_pre_checks" value="true"/>
<stringAttribute key="vdm_launch_config_project" value="RemoteTest"/>
<stringAttribute key="vdm_launch_config_remote_control_class" value="org.overture.remote.ScriptRemote"/>
<booleanAttribute key="vdm_launch_config_remote_debug" value="false"/>
<booleanAttribute key="vdm_launch_config_show_vm_settings" value="false"/>
<booleanAttribute key="vdm_launch_config_static_method" value="false"/>
</launchConfiguration>
-- example script file
create a := new RemoteCall()
-- here is a print function
a.doSomething(1)
-- here is a debug function
a.doSomething(5)
-- and now we quit
quit
class TASTE_Dataview
types
public MyInteger = TASTE_BasicTypes`T_UInt8;
public MyReal = real
inv x ==
x >= 0 and x <= 1000;
public My_Enum = <hello> | <world> | <how_are_you>;
public MySeq ::
a : MySeq_a
b : MySeq_b
c : MySeq_c;
public MyChoice = bool | MySeq;
public MySeqOf = seq of My_Enum
inv x ==
len x = 2;
public MySeqOf2 = seq of My_Enum
inv x ==
len x >= 1 and len x <= 5;
public MyOctStr = seq of char
inv x ==
len x = 3;
public MySeq_c = int
inv x ==
x >= -10 and x <= 10;
public MySeq_b = <taste> | <welcomes> | <you>;
public MySeq_a = seq of MySeq_a_elm
inv x ==
len x >= 1 and len x <= 5;
public MySeq_a_elm = int
inv x ==
x >= 10 and x <= 20
values
public myVar : MySeqOf = [<hello>, <world>];
public myInt : MyInteger = 10;
public myReal : MyReal = 5.500000E+000;
public mychoice : MyChoice = true
end TASTE_Dataview
class TASTE_BasicTypes
types
public T_Int32 = int
inv x ==
x >= -2147483648 and x <= 2147483647;
public T_UInt32 = int
inv x ==
x >= 0 and x <= 4294967295;
public T_Int8 = int
inv x ==
x >= -128 and x <= 127;
public T_UInt8 = int
inv x ==
x >= 0 and x <= 255;
public T_Boolean = bool
values
end TASTE_BasicTypes
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment