(* ****************************************************************** Petstore post_pet: creates a new pet entry - validate input - validation ok --> enter_pet to database - validation error --> raise an application error "pet input not valid" * ******************************************************************) procedure s_post_pet( input ) { pet_post_start: {{^PREFERENCES.debug-output}}\* {{/PREFERENCES.debug-output}} print <<"Pet post, input=", input >>; (* Valid input received *) if ( ~ValidatePetData( input.pet ) ) { pet_application_error( "Invalid input" ); return; }; pet_post_data_valid: (* Referential integrity pet.tag --> tag.tag *) if ( ~ValidTagExists( input.pet.tag ) ) { {{^PREFERENCES.debug-output}}\* {{/PREFERENCES.debug-output}} print <<"Pet post, v_tags=", v_tags >>; pet_application_error( "Tag not found" ); return; }; pet_post_tag_exist: if ( PetStore_GetPetByTag( input.pet.tag ) # {} ) { {{^PREFERENCES.debug-output}}\* {{/PREFERENCES.debug-output}} print <<"Pet post, tag-not free, v_pets=", v_pets >>; pet_application_error( "Tag not free" ); return; }; pet_post_tag_valid_and_used: (* Generate id using infrastructure service /id/{type}(get) *) call infrastructure_id_get( "pet" ); post_pet_id_generated: (* Id generation failure? *) if ( InfrastructureServiceGetStatus( "/id/{type}(get)" ) # "status_200" ) { {{^PREFERENCES.debug-output}}\* {{/PREFERENCES.debug-output}} print <<"Pet post, v_ids=", v_ids >>; pet_application_error( "no id " ); return; }; post_pet_ok: assert( InfrastructureServiceGetStatus( "/id/{type}(get)" ) = "status_200" /\ ValidatePet( New_Pet( input.pet, InfrastructureServiceGetResponse( "/id/{type}(get)" ).id ) ) ); (* Database transaction: create pet *) enter_pet( New_Pet( input.pet, InfrastructureServiceGetResponse( "/id/{type}(get)" ).id )); {{^PREFERENCES.debug-output}}\* {{/PREFERENCES.debug-output}} print <<"Pet post, SUCCESS!!, v_pets=", v_pets >>; pet_post_done: return; }; \* post_pet