Jove
Visualize
Contact Us
JoVE
x logofacebook logolinkedin logoyoutube logo
ABOUT JoVE
OverviewLeadershipBlogJoVE Help Center
AUTHORS
Publishing ProcessEditorial BoardScope & PoliciesPeer ReviewFAQSubmit
LIBRARIANS
TestimonialsSubscriptionsAccessResourcesLibrary Advisory BoardFAQ
RESEARCH
JoVE JournalMethods CollectionsJoVE Encyclopedia of ExperimentsArchive
EDUCATION
JoVE CoreJoVE BusinessJoVE Science EducationJoVE Lab ManualFaculty Resource CenterFaculty Site
Terms & Conditions of Use
Privacy Policy
Policies

Related Concept Videos

Constraints and Statical Determinacy01:26

Constraints and Statical Determinacy

911
In structural engineering, the equilibrium of a system is not only determined by its equations of equilibrium but also with the help of constraints. Constraints refer to restrictions on the motion of a system. The proper combinations of constraints can minimize the total number of constraints needed to maintain a system in mechanical equilibrium. When this happens, the system is said to be statically determinate. For such systems, the unknown reaction supports can be estimated using equilibrium...
911
Mass Analyzers: Common Types01:19

Mass Analyzers: Common Types

1.3K
The quadrupole mass analyzer consists of four cylindrical metal rods arranged in a diamond carrying a DC voltage and a radio-frequency AC voltage. The motion of ions through the quadrupole depends on the field strength, causing only ions of a certain m/z to resonate successfully and strike the detector at a given field strength. Though the transmission rate for these analyzers is high, the exact elemental composition of the sample is not determined because of low resolution; however, they are...
1.3K
Parseval's Theorem01:18

Parseval's Theorem

1.0K
Parseval's theorem is a fundamental concept in signal processing and harmonic analysis. It asserts that for a periodic function, the average power of the signal over one period equals the sum of the squared magnitudes of all its complex Fourier coefficients. This theorem, named after Marc-Antoine Parseval, provides a powerful tool for analyzing the energy distribution in signals.
Interestingly, Parseval's theorem also holds for the trigonometric form of the Fourier series, which expresses a...
1.0K
Mass Analyzers: Overview01:13

Mass Analyzers: Overview

1.5K
The mass analyzer is a crucial component of the mass spectrometer. In the ionization chamber, the vaporized sample is bombarded with a high-energy electron beam to generate a radical cation and further fragment into neutral molecules, radicals, and cations. A series of negatively charged accelerator plates accelerate the cations into the mass analyzer. The mass analyzer separates ions according to their mass-to-charge (m/z) ratios and then directs them to the detector. The common types of mass...
1.5K
Hückel's Rule Diagram of π MOs: Frost Circle01:08

Hückel's Rule Diagram of π MOs: Frost Circle

5.4K
The Frost circle or the inscribed polygon method is a graphical method for determining the relative energies of π molecular orbitals (MOs) for planar, fully conjugated, and monocyclic compounds. This method was first described by A. A. Frost and Boris Musulin in 1953.
A Frost circle is constructed by drawing a polygon whose number of edges is equal to the number of carbons of the given cyclic system, with one of the vertices pointing down. Then, a circle is drawn enclosing the polygon so that...
5.4K
Mathematical Induction01:29

Mathematical Induction

177
Mathematical induction is a structured method of proof used to confirm the truth of statements involving natural numbers. Consider the sum of the first n natural numbers:This formula describes a pattern that appears to hold true as more terms are added. To verify that it is valid for all natural numbers, mathematical induction proceeds in two essential steps. The first is the base case, where the formula is tested for the initial value, typically n = 1. Substituting into both sides confirms the...
177

You might also read

Related Articles

Articles linked to this work by shared authors, journal, and citation graph.

Sort by
Same author

A partial evaluation methodology for optimizing rewrite theories incrementally.

MethodsX·2022
See all related articles

Related Experiment Video

Updated: Jan 3, 2026

Constructing and Visualizing Models using Mime-based Machine-learning Framework
06:19

Constructing and Visualizing Models using Mime-based Machine-learning Framework

Published on: July 22, 2025

2.1K

Imposing assertions in Maude via program transformation.

María Alpuente1, Demis Ballis2, Julia Sapiña1

  • 1VRAIN (Valencian Research Institute for Artificial Intelligence), Universitat Politècnica de València, Camino de Vera s/n, Apdo 22012, 46071 Valencia, Spain.

Methodsx
|November 26, 2019
PubMed
Summary

This study introduces an automated method for correcting Maude programs using program transformation to enforce safety policies. The technique ensures all program computations satisfy specified assertions without removing valid runs.

Keywords:
Assertion enforcementAutomated program transformationEquational rewritingMaudeProgram repairRewriting logicTransformation method for enforcing system invariants in Maude programs

More Related Videos

Applying an eMASS Customization Program as a Research Tool to Evaluate Consumer Benefits
08:27

Applying an eMASS Customization Program as a Research Tool to Evaluate Consumer Benefits

Published on: September 27, 2019

7.2K
Observing the Transformation of Bodily Self-consciousness in the Squeeze-machine Experiment
07:20

Observing the Transformation of Bodily Self-consciousness in the Squeeze-machine Experiment

Published on: March 8, 2019

14.2K

Related Experiment Videos

Last Updated: Jan 3, 2026

Constructing and Visualizing Models using Mime-based Machine-learning Framework
06:19

Constructing and Visualizing Models using Mime-based Machine-learning Framework

Published on: July 22, 2025

2.1K
Applying an eMASS Customization Program as a Research Tool to Evaluate Consumer Benefits
08:27

Applying an eMASS Customization Program as a Research Tool to Evaluate Consumer Benefits

Published on: September 27, 2019

7.2K
Observing the Transformation of Bodily Self-consciousness in the Squeeze-machine Experiment
07:20

Observing the Transformation of Bodily Self-consciousness in the Squeeze-machine Experiment

Published on: March 8, 2019

14.2K

Area of Science:

  • Formal Methods and Program Verification
  • Software Engineering and Program Transformation
  • Automated Program Repair

Background:

  • Program transformation is crucial for generating correct program mutations based on specifications.
  • Existing methods may require dynamic information or lack full automation for program correction.
  • Ensuring safety policies in complex programs like those in Maude is a significant challenge.

Purpose of the Study:

  • To present an automated correction methodology for Maude programs based on program transformation.
  • To enforce a defined safety policy, represented by a set of system assertions (A), on a given Maude program (R).
  • To generate a safe program refinement (R') that satisfies all assertions and preserves original program runs.

Main Methods:

  • The methodology employs automated program transformation for diagnosis and repair of Maude programs.
  • It utilizes a declarative, logical notation for expressing invariant properties and safety constraints as assertions.
  • The approach is static, relying solely on program analysis without requiring runtime error symptoms.

Main Results:

  • A safe program refinement (R') is produced, guaranteeing that all computations satisfy the specified assertions (A).
  • The transformation process ensures that no valid runs (good runs) of the original program (R) are excluded in the refined program (R').
  • The developed methodology is fully automatic, preserving executability requirements.

Conclusions:

  • The automated correction methodology effectively enforces safety policies in Maude programs through static analysis and transformation.
  • The technique offers a declarative way to specify safety constraints, enhancing program verification.
  • This approach provides a robust and efficient solution for generating provably safe program refinements.